\documentclass{article} 
\usepackage{url} 
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb} 
\usepackage{graphicx}
%\usepackage{latexsym}
\usepackage{xcolor} 
%\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}
\usepackage{diagrams}

\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{
\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 

\newcommand{\selfstar}[0]{
$\mathsf{Selfstar}$} 

\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{statement}{Statement}
\newtheorem{assumption}{Assumption}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}

\newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
\newcommand{\lstep}[1]{\to_{\underline{#1}}}
\newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
\newarrowfiller{dasheq} {==}{==}{==}{==}
\newarrow {Mapsto} |--->
\newarrow {Line} -----
\newarrow {Implies} ===={=>}
\newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
\newarrow {Onto} ----{>>}
\newarrow {DashInto} C{dash}{}{dash}{>}
\newarrow {Dashto}{}{dash}{}{dash}{>}
\newarrow {Dashtoo}{}{dash}{}{dash}{>>}


\begin{document}
%\pagestyle{empty}
\title{Type Preservation for \selfstar} 
\author{Peng Fu \\
Computer Science, The University of Iowa}
\date{Last edited: \today}


\maketitle \thispagestyle{empty}

\section{$\mathsf{Selfstar}$}

\subsection{Specifications}
\label{spec}

\noindent \textbf{Conventions}: $x,y, z$ will be used as names for
any variable. $t, a, b$ will be used as names for any term. $L, N,M$ denotes
arbitrary finite non-empty index set. $i,j,k$ denote index variable.
$t_1 \equiv t_2$ means the term (denoted by) $t_1$ is $\alpha$-equivalent to $t_2$, and it also expresses meta level definition unfolding. We are working with terms modulo alpha-equivalence. 

\begin{definition}[Syntax]

\

\noindent \textit{Terms} $t \ :: = * \ | \ x \ | \ \lambda x.t \ |
\ t t' \ | \ \mu t \ | \ \Pi x:t_1.t_2 \ | \ \iota x.t$

\noindent \textit{Closure} $\mu \ ::= \M{x}{t}{N}$

\noindent \textit{Value} $v \ ::= * \ | \ \lambda x.t \ | \ \Pi x:t_1.t_2 \ | \ \iota x.t \ | \ \vec{\mu}(\Pi x:t_1.t_2) \ | \ \vec{\mu}(\iota x.t)$

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:t
\ | \ \Gamma, \tilde{\mu}$

\end{definition} 

Let $\digamma$ denotes the set of context; $\Lambda$ denotes the set of terms. 

\begin{definition}[Typing Rules]

\

\footnotesize{
\begin{tabular}{lll}
    
        \infer[\textit{Star}]{\Gamma \vdash *:*}{}

        &
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&
\infer[\textit{Pi}]{\Gamma \vdash \Pi x:t_1.t_2 : *}{\Gamma,
x: t_1 \vdash t_2 : * & \Gamma \vdash t_1 : * }

\\
\\
\infer[\textit{Self}]{\Gamma \vdash \iota x.t : *}{\Gamma,
x:\iota x.t \vdash t : * }

&
\infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]t'}{\Gamma
\vdash t : \iota x.t'}

&
\infer[\textit{SelfGen}]{\Gamma \vdash t : \iota x.t'}{\Gamma
\vdash t: [t/x]t' & \Gamma \vdash \iota x.t': *}
\\
\\

\infer[\textit{Conv}]{\Gamma \vdash t : t_2}{\Gamma \vdash t:
t_1 & \Gamma \vdash t_1 \cong t_2 & \Gamma \vdash t_2:*}

&
\infer[\textit{Lam}]{\Gamma \vdash \lambda x.t :\Pi x:t_1.
t_2}{\Gamma, x:t_1 \vdash t: t_2 & \Gamma \vdash t_1:*}

&
\infer[\textit{App}]{\Gamma \vdash t t':[t'/x] t_2}{\Gamma
\vdash t:\Pi x:t_1. t_2 & \Gamma \vdash t': t_1}

\\
\\


%% \infer[\textit{O}]{\Gamma \vdash t:  t''}{
%% \Gamma\vdash t: t' & \Gamma \vdash t' =_o t'' }

\infer[\textit{Mu}]{\Gamma \vdash \mu t: \mu t'}{\Gamma, \tilde{\mu}
\vdash t:t' &  \{\Gamma, \tilde{\mu} \vdash t_j: a_j\}_{(t_j:a_j) \in \tilde{\mu}} }

\\
\end{tabular}
}  
\end{definition}

\noindent Let $\cong$ denote $=_o \cup =$, where $=_o$ denote the reflexive transitive symmetry
closure of $\to_o$.

\begin{definition}[Openness of the Closure]
\

  \small{
\begin{tabular}{llll}


\infer{\Gamma \vdash \mu t \to_{o} t}{\mu \in \Gamma}

&


\infer{\Gamma \vdash\lambda x.t \to_{o} \lambda x.t'}{\Gamma
\vdash t \to_{o}t' }

&
\infer{\Gamma \vdash t t' \to_{o} t'' t'}{\Gamma \vdash t
\to_{o}t''}

&

\infer{\Gamma \vdash t t' \to_{o} t t''}{\Gamma \vdash
t'\to_{o}t''}

\\

\\

\infer{\Gamma \vdash \mu t \to_{o} \mu t'}{\Gamma,\tilde{\mu}\vdash t
\to_{o}t' }

&

\infer{\Gamma \vdash \iota x.t \to_{o} \iota x.t'}{\Gamma
\vdash t \to_{o}t' }
&

\infer{\Gamma \vdash \Pi x:t_1.t_2 \to_{o} \Pi
x:t_1'.t_2'}{\Gamma \vdash t_2 \to_{o}t_2' } 

&
\infer{\Gamma \vdash \Pi x:t_1.t_2 \to_{o} \Pi
x:t_1'.t_2'}{\Gamma \vdash t_1 \to_{o}t_1' } 
\\
\end{tabular}
}

\end{definition}


\begin{definition}[Executions]

\

\footnotesize{
  \begin{tabular}{lllll}

 \infer{\Gamma \vdash\vec{\mu} * \leadsto *}{}

&
 \infer{\Gamma \vdash x_i \leadsto  t_i}{(x_i \mapsto t_i) \in
\Gamma}

&

 \infer{\Gamma \vdash \vec{\mu} x_i \leadsto  \vec{\mu} t_i}{(x_i \mapsto t_i) \in
\mu \in \vec{\mu}}

&
\infer{\Gamma \vdash\vec{\mu}(t t') \leadsto
(\vec{\mu}t)(\vec{\mu}t')}{ }

&
\infer{\Gamma \vdash\vec{\mu} x \leadsto  x}{x \notin
dom(\vec{\mu}) }

\\
\\
\infer{\Gamma \vdash\vec{\mu}(\lambda x.t) \leadsto \lambda
x.(\vec{\mu}t)}{ }

&
\infer{\Gamma \vdash(\lambda x.t)v\leadsto [v/x]t}{}

&
\infer{\Gamma \vdash t t' \leadsto t'' t'}{\Gamma \vdash t
\leadsto t''}

&
\infer{\Gamma \vdash(\lambda x.t) t' \leadsto (\lambda x.t)
t''}{\Gamma \vdash t'\leadsto t''}
&



\\
\end{tabular}
}

\end{definition}


\begin{definition}[Equality]
\

\footnotesize{
\begin{tabular}{llll}

\infer{\Gamma \vdash t_1= t_2}{\Gamma \vdash t_1
{\leadsto^*} t_2}

&
\infer{\Gamma \vdash(\lambda x.t)t' = [t'/x]t}{}

&
\infer{\Gamma \vdash t_1 =  t_3}{\Gamma \vdash t_2 =  t_3
&\Gamma \vdash t_1 =  t_2}

&
\infer{\Gamma \vdash t_1 =  t_2}{\Gamma \vdash t_2 = t_1 }

\\

\\
\infer{\Gamma \vdash\mu (\iota x.t) =\iota x.(\mu t')}{}

&
\infer{\Gamma \vdash\mu (\Pi x:t_1.t_2) =\Pi x:\mu t_1. \mu
t_2}{}

&
\infer{\Gamma \vdash\lambda x.t = \lambda x.t'}{\Gamma \vdash t
=t' }

&

\infer{\Gamma \vdash\iota x.t = \iota x.t'}{\Gamma \vdash t =t'
}

\\

\\
\infer{\Gamma \vdash\Pi x:t_1.t_2 = \Pi x:t_1'.t_2'}{\Gamma
\vdash t_1 =t_1' &\Gamma \vdash t_2 = t_2'}

&
\infer{\Gamma \vdash\mu t =\mu t'}{\Gamma,\tilde{\mu} \vdash t=t' }

    &
\infer{\Gamma \vdash t t' = t'' t'''}{\Gamma \vdash t=t''
&\Gamma \vdash t' = t'''}

&

\infer{\Gamma \vdash \mu t = t }{ \mathsf{FV}(t)\#
dom(\mu)}


\\
\end{tabular}
}
  
\end{definition}


\noindent \textbf{Remarks} :

\begin{itemize}
  
  \item $\tilde{\_}$ is an operation on clousure. If $\mu$ is $\M{x}{t}{N}$, then $\tilde{\mu}$ is $\bm{x}{a}{t}{N}$.

    \item  For $\M{x}{t}{N}$, we
require for any $ 1 \leq i \leq n $, $\mathsf{FV}(t_i) \subseteq dom(\mu) = \{
x_1,..., x_n\}$. %% and each $t_i$ is \textit{pure}(i.e. does not contain any closure),  we call this requirement \textit{local property}. The motivation of purity requirement come from the following intuition: when ever $\mu_1, \Gamma_1, \{ x \mapsto \mu_1 y\}$, then we can reformulate it
%% as $\Gamma_1, \mu_1 \cup \{ x \mapsto y\}$. Purity is used in the proof of lemma \ref{erase:eq}.
Locality is a very important property that will be assumed or used through out this draft. On the other hand, without locality requirement, we predict it is very difficult to analyze the type system with mutual recursion. 

\item $\mu \in t$ means the closure $\mu$ appears in $t$. $\vec{\mu}t$ denotes $\mu_1...\mu_n t$. $\vec{\mu}$ here and through out this article is not allowed to be an empty closure. We do have a notation for allowing possibly empty many closure, namely, $\dot{\vec{\mu}}$. 

\item $(t_i : a_i) \in \tilde{\mu}$ means $(x_i:a_i) \mapsto t_i \in \tilde{\mu}$. $x_i \mapsto t_i \in \tilde{\mu}$ means $(x_i:a_i) \mapsto t_i \in \tilde{\mu}$.

\item $[t'/x](\mu t )\ \equiv \mu([t'/x]t)$ and
$[t'/x](\iota y.t )\ \equiv \iota y. [t'/x]t$.

\item For the following two rules: 

\

\begin{tabular}{lll}
\infer{\Gamma \vdash \mu t = t }{ \mathsf{FV}(t)\#
dom(\mu)}

&

\infer{\Gamma \vdash \vec{\mu} x = \mu x }{ x \in
dom(\mu)}
\end{tabular}

\noindent \textbf{Note}: I choose the first one for the sake of \textit{syntax uniformity}. I use a single $\mu$
everywhere in the definition of equality, it would seems odd to use $\vec{\mu}$ for one rule. 
For the same reason I choose the form of Mu reductions in next section, it is already 
nondeterministic since we allow mu reduction underneath the mu, adding this kind of
rule will of course make it \textit{more} nondeterministic. In another words, I prefer uniformity over deterministicness. 

\end{itemize}

\subsection{Analytical System}


\begin{definition}[Beta Reductions]

\

\small{
\begin{tabular}{llll}


\infer{\Gamma \vdash x \to_{\beta} t}{(x\mapsto t) \in \Gamma}

&
\infer{\Gamma \vdash(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

\infer{\Gamma \vdash\mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto
t_i) \in \mu}

&

\infer{\Gamma \vdash\lambda x.t \to_{\beta} \lambda x.t'}{\Gamma
\vdash t \to_{\beta}t' }

\\

\\
\infer{\Gamma \vdash t t' \to_{\beta} t'' t'}{\Gamma \vdash t
\to_{\beta}t''}

&

\infer{\Gamma \vdash t t' \to_{\beta} t t''}{\Gamma \vdash
t'\to_{\beta}t''}

&

\infer{\Gamma \vdash \mu t \to_{\beta} \mu t'}{\Gamma,\tilde{\mu}\vdash t
\to_{\beta}t' }

&

\infer{\Gamma \vdash \iota x.t \to_{\beta} \iota x.t'}{\Gamma
\vdash t \to_{\beta}t' }
\\
\\

\infer{\Gamma \vdash \Pi x:t_1.t_2 \to_{\beta} \Pi
x:t_1'.t_2'}{\Gamma \vdash t_2 \to_{\beta}t_2' } 

&
\infer{\Gamma \vdash \Pi x:t_1.t_2 \to_{\beta} \Pi
x:t_1'.t_2'}{\Gamma \vdash t_1 \to_{\beta}t_1' } 
\\
\end{tabular}
}
  
\end{definition}

\begin{definition}[Mu Reductions]

\

\small{
\begin{tabular}{llll}


\infer{ \Gamma \vdash \mu t \to_{\mu} t}{dom(\mu) \#
\mathsf{FV}(t)}

&
\infer{ \Gamma \vdash \mu(\lambda x.t) \to_{\mu} \lambda x.\mu
t}{}

&

\infer{ \Gamma \vdash \mu(t_1 t_2)  \to_{\mu} (\mu t_1 ) (\mu
t_2)}{}

&

\infer{ \Gamma \vdash \mu(\iota x.t) \to_{\mu} \iota x.\mu t}{}

\\

\\
\infer{ \Gamma \vdash \mu(\Pi x:t_1.t_2) \to_{\mu} \Pi x:\mu
t_1.\mu t_2}{}

&
\infer{ \Gamma \vdash \lambda x.t \to_{\mu} \lambda x.t'}{\Gamma
\vdash t \to_{\mu} t'}

&
\infer{ \Gamma \vdash t t' \to_{\mu} t t''}{ 
\Gamma \vdash t'\to_{\mu} t''}

&
\infer{ \Gamma \vdash t t' \to_{\mu} t'' t'}{ \Gamma \vdash t
\to_{\mu} t''}

\\

\\
\infer{\Gamma \vdash  \Pi x:t_1 t_2 \to_{\mu} \Pi x:t_1.
t_2'}{ \Gamma \vdash t_1 \to_{\mu} t_1'}

&
\infer{\Gamma \vdash  \iota x.t \to_{\mu} \iota x.t'}{\Gamma
\vdash t \to_{\mu} t'}

&
\infer{ \Gamma \vdash \Pi x:t_1 t_2 \to_{\mu} \Pi x:t_1.
t_2'}{ \Gamma \vdash t_2 \to_{\mu} t_2'}

&
\infer{ \Gamma \vdash \mu t \to_{\mu} \mu t'}{\Gamma,\tilde{\mu}\vdash t
\to_{\mu}t' }

\\
\end{tabular}
}  
\end{definition}

\noindent \textbf{Note}: It may seem that the rules: 

\

\begin{tabular}{lll}
\infer{ \Gamma \vdash \mu t \to_{\mu} \mu t'}{\Gamma,\tilde{\mu}\vdash t
\to_{\mu}t' }

&

\infer{\Gamma \vdash \mu t \to_{\beta} \mu t'}{\Gamma,\tilde{\mu}\vdash t
\to_{\beta}t' }
&  
\infer{\Gamma \vdash\mu t =\mu t'}{\Gamma,\tilde{\mu} \vdash t=t' }

\end{tabular}

\

\noindent are not different from others, but this way of setting up the congruence 
over the closure actually is important for proving lemma \ref{metacong}(which is used in
the final preservation proof). 

\subsection{Confluence of Analytical System}
\label{confluence}
 The confluence argument is similar to the one described in \cite{CurienHL96}. We are going to use the following lemma to conclude the confluence of $\to_{\beta} \cup \to_{\mu}$.

\begin{lemma}[Interpretation lemma]
\label{interp}
Let $\mathcal{R} = \mathcal{R}_1 \cup \mathcal{R}_2$ be the union of two relations, 
$\mathcal{R}_1$ being confluent and strongly normalizing. We denote by $\mathcal{R}_1(a)$ the $\mathcal{R}_1$-normal form of $a$. Suppose that there is some relation $\mathcal{R}'$ on $\mathcal{R}_1$ normal forms satisfying:

\

$\mathcal{R}' \subseteq \mathcal{R}^*$ and 

$a \stackrel{\mathcal{R}_2}{\to} b $ implies $ \mathcal{R}_1(a)  \stackrel{\mathcal{R}'^*}{\to}   \mathcal{R}_1(b)$ $\dagger$

\

\noindent Then the confluence of $\mathcal{R}'$ implies the confluence of $\mathcal{R}$.
\end{lemma}

\begin{proof}
 So suppose $\mathcal{R}'$ is confluent. Suppose $a \stackrel{\mathcal{R}^*}{\to} a'$ and $a \stackrel{\mathcal{R}^*}{\to} a''$. So by $\dagger$, $\mathcal{R}_1(a) \stackrel{\mathcal{R}'^*}{\to} \mathcal{R}_1(a')$ and $\mathcal{R}_1(a) \stackrel{\mathcal{R}'^*}{\to} \mathcal{R}_1(a'')$. Notice that $t \stackrel{\mathcal{R}_1^*}{\to} t'$ implies $\mathcal{R}_1(t) = \mathcal{R}_1(t')$(By confluence and strong normalization of $\mathcal{R}_1$). By confluence of $\mathcal{R'}$, there exists $b$ such that $\mathcal{R}_1(a') \stackrel{\mathcal{R}'^*}{\to} b$ and $\mathcal{R}_1(a'') \stackrel{\mathcal{R}'^*}{\to} b$. Since $\mathcal{R}', \mathcal{R}_1 \subseteq \mathcal{R}^*$, we get $a'\stackrel{\mathcal{R}^*}{\to}  \mathcal{R}_1(a') \stackrel{\mathcal{R}^*}{\to} b$ and $a''\stackrel{\mathcal{R}^*}{\to}  \mathcal{R}_1(a'') \stackrel{\mathcal{R}^*}{\to} b$. Hence $\mathcal{R}$ is confluent.
\end{proof}

\begin{lemma}
  $\to_{\mu}$ is terminating.
\end{lemma}

\begin{lemma}
  $\to_{\mu}$ is confluent.
\end{lemma}

\begin{definition}[$\mu$-Normal Forms]
  \label{mu-normal}
\

\noindent $n \ :: = * \ | \ x \ | \   \mu x_i \ | \ \lambda x.n \ | \ n n'\ | \ \Pi x:n.n' \ | \ \iota x.n$

\end{definition}

\noindent  \textbf{Note}: for the $\mu x_i$ in definition \ref{mu-normal}, we assume $x_i \in dom(\mu)$. We define the $\mu$ normalization function $m(t)$ as below.

\begin{definition}

    \

\small{
    \begin{tabular}{lll}

  $ m(*) \ : = \ * $

  &
  $ m(x) \ : = \  x$

&

  $m(\lambda y.t)\ : = \ \lambda y.m(t)$

\\
  $m(t_1 t_2)\ : = \ m(t_1) m(t_2)$
&

  $m(\iota x.t)\ : = \ \iota x. m(t)$
&
  $m(\Pi x:t.t') \ := \Pi x:  m(t). m(t')$.
\\
  $ m(\vec{\mu}y) \ := y$ if $y \notin dom(\vec{\mu})$.

&
  $ m(\vec{\mu}y) \ := \mu_i y$ if $y \in dom(\mu_i)$.

&
  $m(\vec{\mu}(t t')) \ :=  m(\vec{\mu} t) m( \vec{\mu}t')$

\\
  $m(\vec{\mu}( \lambda x.t)) \ := \lambda x.  m(\vec{\mu}t)$.

&
  $m(\vec{\mu}( \iota x.t)) \ := \iota x.  m(\vec{\mu}t)$.

&
  $m(\vec{\mu}( \Pi x:t.t')) \ := \Pi x:  m(\vec{\mu}t). m(\vec{\mu}t')$.
\\

\end{tabular}
}
\end{definition}

\noindent \textbf{Note}: $\vec{\mu}$ here and through out this article is not allowed to be an empty closure, this decision is based on two reasons: 1. Trying to be consistent with the operational semantics, where allowing $\vec{\mu}$ to contains empty closure will result reflexiveness for the operational semantics. 2. It will increase the cognitive burden for understanding this
article, which is already a lot. 

\begin{lemma}
\label{norm:fun}
 Let $\Phi$ denote the set of $\mu$ normal form. For any term $t$, $m(t)\in \Phi$.
\end{lemma}
\begin{proof}
  One way to prove this is first identify $t$ as $\dot{\overrightarrow{\mu_1}}t'$, here $\dot{\overrightarrow{\mu_1}}$ means
there are zero or more closures and $t'$ does not contains any closure at head position.
 Then we can proceed by induction on the structure of $t'$:

\

\noindent \textbf{Base Cases}: $t' = x$, $t' = *$, obvious.

\

\noindent \textbf{Step Cases}: If $t' = \lambda x.t''$, 
then $m(\dot{\overrightarrow{\mu_1}}(\lambda x.t'')) \equiv \lambda x.m(\dot{\overrightarrow{\mu_1}} t'')$. Now we can
again identify $t''$ as $\dot{\overrightarrow{\mu_2}} t'''$, where $t'''$ does not have any closure at head position. Since $t'''$ is structurally smaller than $\lambda x.t''$, by IH, $m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}} t''') \in \Phi$, thus $m(\dot{\overrightarrow{\mu_1}}(\lambda x.t'')) \equiv \lambda x.m(\dot{\overrightarrow{\mu_1}} t'') \in \Phi$.

For $t' = t_a t_b$, $t' = \iota x.t''$, $t' = \Pi x:t_a.t_b$, we can argue similarly as above.
\end{proof}

\begin{lemma}
\label{norm:id}
  If $n \in \Phi$, then $m(n) \equiv n$. 
\end{lemma}
\begin{proof}
  By induction on the structure of $n$. 
\end{proof}

\begin{definition}[$\beta$ Reduction on $\mu$-normal Forms]

\
  
\infer{\Gamma \vdash n \to_{\beta \mu} m(t)}{\Gamma \vdash n \to_{\beta}t}

\end{definition}

\noindent \textbf{Note}: From this definition we can conclude: 

\

\begin{tabular}{lll}

\infer{\Gamma \vdash \lambda x.n \to_{\beta \mu} \lambda x.n'}{\Gamma \vdash n \to_{\beta \mu} n' }

&

\infer{\Gamma \vdash n n' \to_{\beta \mu} n n''}{\Gamma \vdash n' \to_{\beta \mu} n'' }

&
\infer{\Gamma \vdash n n' \to_{\beta \mu} n'' n'}{\Gamma \vdash n \to_{\beta \mu} n'' }
\\
\\
\infer{\Gamma \vdash \iota x.n \to_{\beta \mu} \iota x.n'}{\Gamma \vdash n \to_{\beta \mu} n' }

&
\infer{\Gamma \vdash \Pi x:n.n' \to_{\beta \mu} \Pi x: n''.n'}{\Gamma \vdash n \to_{\beta \mu} n'' }

&
\infer{\Gamma \vdash \Pi x:n.n' \to_{\beta \mu} \Pi x:n.n''}{\Gamma \vdash n' \to_{\beta \mu} n'' }

\\
\end{tabular}

\

\noindent The first rule follows because: Assume $\Gamma \vdash n \to_{\beta\mu} n'$, say $m(t) \equiv n'$ and $\Gamma \vdash n \to_{\beta} t$. Then $\Gamma \vdash \lambda x.n \to_{\beta} \lambda x.t$ and $m(\lambda x.t) \equiv \lambda x.m(t) \equiv \lambda x.n'$. The others follow similarly. 


\begin{lemma}
\label{subj}
If $\Gamma \vdash   n_1\to_{\beta\mu} n_1'$, then $\Gamma \vdash m([n_2/x]n_1) \to_{\beta\mu} m([n_2/x]n_1')$.
\end{lemma}
\begin{proof}
  By induction on derivation of $\Gamma \vdash   n_1\to_{\beta} t_1$, where $m(t_1) \equiv n_1'$.
We will list a few nontrivial cases. Note that the we use lemma \ref{norm:iden} implicitly. 

\

\noindent \textbf{Base Case}:

\

\infer{\Gamma \vdash y \to_{\beta} t_1}{(y\mapsto t_1) \in \Gamma}

\

\noindent In this case $n_1 = y$. By locality, we have $\Gamma \vdash m([n_2/x]y) \equiv y \to_{\beta\mu} m(t_1) \equiv m([n_2/x]t_1)$.


\

\noindent \textbf{Base Case}: 

\

\infer{\Gamma \vdash(\lambda y.n)n' \to_{\beta} [n'/y]n}{}

\

\noindent $n_1 = (\lambda y.n)n'$. So $\Gamma \vdash m([n_2/x]((\lambda y.n)n')) \equiv m((\lambda y.[n_2/x]n) [n_2/x]n') \equiv (\lambda y.m([n_2/x]n)) m([n_2/x]n')  \to_{\beta\mu}m([m([n_2/x]n')/y] m([n_2/x]n)) \equiv m([[n_2/x]n'/y] ([n_2/x]n)) \equiv m([n_2/x]([n'/y]n))$. 

\

\noindent \textbf{Base Case}: 

\

\infer{\Gamma \vdash\mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto
t_i) \in \mu}

\

\noindent $n_1 = \mu x_i$. By locality, $\Gamma \vdash m([n_2/x]\mu x_i) \equiv \mu x_i \to_{\beta\mu} m(\mu t_i) \equiv m([n_2/x](\mu t_i))$.


\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash\lambda y.n \to_{\beta} \lambda y.t'}{\Gamma
\vdash n \to_{\beta}t' }

\

\noindent $n_1 = \lambda y.n$. By IH, we have $\Gamma\vdash m([n_2/x]n)  \to_{\beta\mu} m([n_2/x]t')$. So $\Gamma\vdash m(\lambda y.[n_2/x]n)  \to_{\beta\mu} m(\lambda y.[n_2/x]t')$.

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \mu t \to_{\beta} \mu t'}{\Gamma,\tilde{\mu}\vdash t
\to_{\beta}t' }

\

\noindent This case will not arise since $n_1$ is already in $\mu$ normal form.

\

\noindent The other cases are similar.
 
\end{proof}
\begin{lemma}
\label{subp}
If $\Gamma \vdash n_2\to_{\beta\mu} n_2'$, then $\Gamma \vdash m([n_2/x]n_1) \stackrel{*}{\to_{\beta\mu}} m([n_2'/x]n_1)$.
\end{lemma}
\begin{proof}
  By induction on $n_1$.
\end{proof}

\begin{definition}
  We say $x$ is unsubstitutable w.r.t. $\Gamma$ if there is some $t, a$ such that $(x:a) \mapsto t \in \Gamma$. 
\end{definition}

\noindent \textbf{Note}: If $x$ is not unsubstitutable, we say it is substitutable, in this draft we assume for any substitution $[t/x]$, $x$ is substitutable w.r.t. $\Gamma$.



\begin{definition}[Parallel Reductions]

\

  \begin{tabular}{lllll}


\infer{\Gamma \vdash  n \Rightarrow_{\beta \mu} n}{}

&

&
\infer{\Gamma \vdash  x \Rightarrow_{\beta\mu} m( t)}{(x \mapsto t) \in \Gamma}

&

&
\infer{\Gamma \vdash \mu x_i \Rightarrow_{\beta\mu} m(\mu t_i)}{(x_i \mapsto t_i) \in \mu}

\\

\\

\infer{\Gamma \vdash (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} m([n_2'/x]n_1')}{\Gamma \vdash   n_1\Rightarrow_{\beta\mu} n_1' &\Gamma \vdash  n_2\Rightarrow_{\beta\mu} n_2'}

&
&

\infer{\Gamma \vdash \lambda x.n \Rightarrow_{\beta\mu} \lambda x.n'}{\Gamma \vdash n \Rightarrow_{\beta\mu}n' }

&
&
\infer{\Gamma \vdash n n' \Rightarrow_{\beta\mu} n'' n'''}{ \Gamma \vdash  n \Rightarrow_{\beta\mu}n''& \Gamma \vdash n' \Rightarrow_{\beta\mu} n'''}

\\
\\

\infer{\Gamma \vdash \iota x.n \Rightarrow_{\beta\mu} \iota x.n'}{\Gamma \vdash n \Rightarrow_{\beta\mu}n' }
&
&
\infer{\Gamma \vdash \Pi x:n.n' \Rightarrow_{\beta\mu} \Pi x:n''.n'''}
{\Gamma \vdash n' \Rightarrow_{\beta\mu} n''' &\Gamma \vdash  n \Rightarrow_{\beta\mu}n'' }
\\

\end{tabular}

\end{definition}

\begin{lemma}
  $\to_{\beta\mu} \subseteq \Rightarrow_{\beta\mu} \subseteq \to_{\beta\mu}^*$.
\end{lemma}
\begin{proof}
  %% Many proofs involving parallelization typically state this lemma as obvious result. Obviousness arises in many situations, sadly this is not one of them. Thus I include a proof sketch here.

For $\to_{\beta\mu} \subseteq \Rightarrow_{\beta\mu}$, by induction on the derivation of
$\Gamma \vdash n \to_{\beta} t$, where $\Gamma \vdash n \to_{\beta\mu} m(t)$.

For $\Rightarrow_{\beta\mu} \subseteq \to_{\beta\mu}^*$, by induction on the derivation of
$\Gamma \vdash n \Rightarrow_{\beta\mu} n'$. We show the case where(the other cases are obvious): 

\

\infer{\Gamma \vdash (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} m([n_2'/x]n_1')}{\Gamma \vdash   n_1\Rightarrow_{\beta\mu} n_1' &\Gamma \vdash  n_2\Rightarrow_{\beta\mu} n_2'}

\

\noindent By lemma \ref{key}, we know that $\Gamma \vdash m([n_2/x]n_1) \Rightarrow_{\beta\mu} m([n_2/x]n_1)$, given $\Gamma \vdash   n_1\Rightarrow_{\beta\mu} n_1' ,\Gamma \vdash  n_2\Rightarrow_{\beta\mu} n_2'$. Since $\to_{\beta\mu} \subseteq \Rightarrow_{\beta\mu}$, we have: if $\Gamma \vdash   n_1\to_{\beta\mu} n_1', \Gamma \vdash  n_2\to_{\beta\mu} n_2'$ , then $\Gamma \vdash m([n_2/x]n_1) \to_{\beta\mu} m([n_2'/x]n_1')$($\dagger$). By IH, we have $\Gamma \vdash   n_1\stackrel{*}{\to_{\beta\mu}} n_1' ,\Gamma \vdash  n_2 \stackrel{*}{\to_{\beta\mu}}n_2'$. By lemma \ref{subj}, lemma \ref{subp} and ($\dagger$), we have $\Gamma \vdash (\lambda x.n_1)n_2 \to_{\beta\mu} m([n_2/x]n_1) \stackrel{*}{\to_{\beta\mu}} m([n_2'/x]n_1')$.

\end{proof}
\begin{lemma}
\label{lemma7}
If $\Gamma \vdash n_2 \Rightarrow_{\beta\mu} n_2'$, then $\Gamma \vdash m([n_2/x]n_1) \Rightarrow_{\beta\mu} m([n_2'/x]n_1)$.
\end{lemma}

\begin{proof}
\noindent  By induction on the structure of $n_1$. 

\

\noindent \textbf{Base Cases}: $n_1= x$, $n_1 = \mu x_i$, $n_1 = *$. Obvious. 

\

\noindent \textbf{Step Case}: $n_1= \lambda y.n$. We have $\Gamma \vdash m(\lambda y.[n_2/x]n) \equiv \lambda y.m([n_2/x]n) \stackrel{IH}{\Rightarrow_{\beta\mu}} \lambda y.m([n_2'/x]n) \equiv m(\lambda y.[n_2'/x]n)$.

\

\noindent \textbf{Step Case}: $n_1= n n'$. We have $\Gamma \vdash m([n_2/x]n [n_2/x]n') \equiv m([n_2/x]n) m([n_2/x]n')\stackrel{IH}{\Rightarrow_{\beta\mu}} m([n_2'/x]n) m([n_2'/x]n')\equiv m([n_2'/x]n[n_2'/x]n)$.

\

\noindent \textbf{Step Case}: $n_1 = \iota x.n, \Pi x:n.n'$. Similar as above.

\end{proof}

\begin{lemma}
\label{norm:iden}
 $m(m(t)) \equiv m(t)$ and $m([m(t_1)/y] m(t_2)) \equiv m([t_1/y]t_2)$. 
\end{lemma}
\begin{proof}
The first equality is by lemma \ref{norm:id} and lemma \ref{norm:fun}. For the second equality, we 
prove it using similar method as lemma \ref{norm:fun}: We identify $t_2$ as $\dot{\overrightarrow{\mu_1}}t_2'$, where $t_2'$ does not contains any closure at head position. We proceed by induction on the structure of $t_2'$:

\

\noindent \textbf{Base Cases}: $t_2' = *$, obvious. For $t_2' = x$, we use $m(m(t)) \equiv m(t)$. 

\

\noindent \textbf{Step Cases}: If $t_2' = \lambda x.t_2''$, 
then $m(\dot{\overrightarrow{\mu_1}}(\lambda x.[t_1/y]t_2'')) \equiv \lambda x.m(\dot{\overrightarrow{\mu_1}}([t_1/y]t_2'')) \equiv \lambda x.m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}([t_1/y]t_2'''))$, where $t_2''$ is identified as $\dot{\overrightarrow{\mu_2}} t_2'''$, and $t_2'''$ does not have any closure at head position. Since $t_2'''$ is structurally smaller than $\lambda x.t_2''$, by IH, $m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}([t_1/y]t_2''')) \equiv m([t_1/y](\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}t_2''')) \equiv m([m(t_1)/y] m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}t_2'''))$. Thus $\lambda x.m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}([t_1/y]t_2''')) \equiv \lambda x. m([m(t_1)/y] m(\dot{\overrightarrow{\mu_1}}\dot{\overrightarrow{\mu_2}}t_2'''))$, implying $m([t_1/y]\dot{\overrightarrow{\mu_1}}(\lambda x.t_2'')) \equiv m( [m(t_1)/y] m(\lambda x.\dot{\overrightarrow{\mu_1}}t_2''))$. Since $m( [m(t_1)/y] m(\lambda x.\dot{\overrightarrow{\mu_1}}t_2'')) \equiv m( [m(t_1)/y] m(\dot{\overrightarrow{\mu_1}}(\lambda x.t_2'')))$, we conclude 

\noindent $m( [m(t_1)/y] m(\dot{\overrightarrow{\mu_1}}(\lambda x.t_2''))) \equiv m([t_1/y]\dot{\overrightarrow{\mu_1}}(\lambda x.t_2'')) $.

For $t_2' = t_a t_b$, $t_2' = \iota x.t_2''$, $t_2' = \Pi x:t_a.t_b$, we can argue similarly as above.



\end{proof}
\begin{lemma}
\label{key}
If $\Gamma \vdash n_1 \Rightarrow_{\beta\mu} n_1'$ and $\Gamma \vdash n_2 \Rightarrow_{\beta\mu} n_2'$, then $\Gamma \vdash m([n_2/y]n_1) \Rightarrow_{\beta\mu} m([n_2'/y]n_1')$.
\end{lemma}

\begin{proof}

\noindent We prove this by induction on the derivation of $\Gamma \vdash n_1 \Rightarrow_{\beta\mu} n_1'$.
  
\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash n \Rightarrow_{\beta \mu} n}{}

\

\noindent By lemma \ref{lemma7}.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash \mu x_i\Rightarrow_{\beta\mu} m(\mu t_i)}{x_i \mapsto t_i \in \mu}

\

\noindent Since $y \notin \mathsf{FV}(\mu x_i)$ and $\mu$ is local, $m([n_2/y]\mu x_i) \equiv m(\mu x_i)$, then $m(\mu x_1) \equiv \mu x_i \Rightarrow_{\beta\mu} m(\mu t_i) \equiv m(m(\mu t_i))$(lemma \ref{norm:iden}). 

\

\noindent \textbf{Base Case:}

\

\infer{\Gamma \vdash  x \Rightarrow_{\beta\mu} m( t)}{(x \mapsto t) \in \Gamma}

\

\noindent In this case, $x$ is unsubstitutable. So this situation will not arise. (\textbf{Note}: Prof. Stump suggested that we may assume $x \not \equiv y$, then we may have $m([n_2/y]x) \equiv m(x) \equiv x \Rightarrow_{\beta\mu} m(t) \equiv m(m(t)) \equiv m([n_2/y]m(t))$. So in this sense we can use locality to replace the need for the notion of \textit{substitutability}.)

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash (\lambda x.n_a) n_b \Rightarrow_{\beta\mu} m([n_a'/x]n_b')}{\Gamma \vdash n_a\Rightarrow_{\beta\mu} n_a' & \Gamma \vdash n_b\Rightarrow_{\beta\mu} n_b'}

\

\noindent We have $\Gamma \vdash m((\lambda x.[n_2/y]n_a) [n_2/y] n_b) \equiv (\lambda x.m([n_2/y]n_a)) m([n_2/y] n_b)$

$ \stackrel{IH}{\Rightarrow_{\beta\mu}} m([m([n_2'/y] n_b')/x]m([n_2'/y] n_a')) \equiv m([n_2'/y]([n_b'/x]n_a'))$. The last equality is by lemma \ref{norm:iden}. Here we first apply induction hypothesis to reduce, then apply ${\Rightarrow_{\beta\mu}}$.

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash \lambda x.n \Rightarrow_{\beta\mu} \lambda x.n'}{\Gamma \vdash n \Rightarrow_{\beta\mu}n' }

\

\noindent We have $\Gamma \vdash m(\lambda x.[n_2/y]n) \equiv \lambda x.m([n_2/y]n) \stackrel{IH}{\Rightarrow_{\beta\mu}} \lambda x.m([n_2'/y]n') \equiv m(\lambda x.[n_2'/y]n') $

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash n_a n_b \Rightarrow_{\beta\mu} n_a'n_b'}{ \Gamma \vdash n_a\Rightarrow_{\beta\mu} n_a' & \Gamma \vdash n_b\Rightarrow_{\beta\mu} n_b'}

\

\noindent We have $\Gamma \vdash m([n_2/y]n_a [n_2/y] n_b) \equiv m([n_2/y]n_a) m([n_2/y] n_b)$

$ \stackrel{IH}{\Rightarrow_{\beta\mu}} m([n_2'/y] n_a') m([n_2'/y] n_b')\equiv m([n_2'/y](n_a'n_b'))$.

\

\noindent The other cases are similar as above. 

\end{proof}

\noindent \textbf{Note}: Since we define a similar notion of parallel reduction as 
Tait-Martin L\"of's, the curious reader may ask if we can use Takahashi's notion of complete development \cite{Takahashi95} to show confluence. I would not do this based on following reason:

\

\noindent It introduces a new concept(or function), namely, \textit{complete development}. If it is a short draft, I would
possibly consider it, but it is a long draft(included already a lot of heavy concepts), to maintain a weak sense
of \textit{simplicity}, I would not adopt it here. Of course it could be an interesting investigation and I would leave this exploration to my dissertation work.

%% \noindent 2. We would define the function $\_^*$ inductively on normal $\mu$ term $n$, we will need to define $((\lambda x.n_1) n_2)^* := m([n_2^*/x]n_1^*)$.

%% \

%% \noindent 3. Suppose we want to use the notion of complete development \`a la Takahashi, we would need to show this lemma:
%% if $\Gamma \vdash n_1 \Rightarrow_{\beta\mu} n_2$, then $\Gamma \vdash n_1 \Rightarrow_{\beta\mu} n_2^*$. This means
%% that at least you would need to investigate the behaviors of $(m(t))^*$ for some $t$ since we can have this reduction: $\Gamma \vdash x \Rightarrow_{\beta\mu} m(t)$ for $x\mapsto t \in \Gamma$. Say $\Gamma \vdash x \Rightarrow_{\beta\mu} (\lambda y.n)n'$, we would need to show $\Gamma \vdash x \Rightarrow_{\beta\mu} ((\lambda y.n)n')^* \equiv m([n'^*/y]n^*)$. $x$ can not possibly one step $\Rightarrow_{\beta\mu}$ to $m([n'^*/y]n^*)$.

%% \

%% \noindent So Takahashi's method at least will not simply the proofs in our system. That's why I adopt a direct 
%% proof of diamond property. 

\


\begin{lemma}[Diamond Property] 
  If $ \Gamma \vdash n \Rightarrow_{\beta\mu} n'$ and $\Gamma \vdash n \Rightarrow_{\beta\mu} n''$, then there exist $n'''$ such that $ \Gamma \vdash n'' \Rightarrow_{\beta\mu} n'''$ and $ \Gamma \vdash n' \Rightarrow_{\beta\mu} n'''$.
\end{lemma}

\begin{proof}
  \noindent By induction on the derivation of $\Gamma \vdash n \Rightarrow_{\beta\mu} n'$. 

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash n \Rightarrow_{\beta \mu} n}{}

\

\noindent Obvious.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash x \Rightarrow_{\beta\mu} m( t)}{(x \mapsto t) \in \Gamma}

\

\noindent Obvious.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash \mu x_i\Rightarrow_{\beta\mu} m(\mu t_i)}{}

\

\noindent Obvious. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} m([n_2'/x]n_1')}{ \Gamma \vdash n_1\Rightarrow_{\beta\mu} n_1' &\Gamma \vdash n_2\Rightarrow_{\beta\mu} n_2'}

\

\noindent Suppose $\Gamma \vdash (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu}(\lambda x.n_1'') n_2''$, where $\Gamma \vdash n_1 \Rightarrow_{\beta\mu}n_1''$ and $\Gamma \vdash n_2 \Rightarrow_{\beta\mu} n_2''$. By IH, there exist $n_1''', n_2'''$ such that $\Gamma \vdash n_1'' \Rightarrow_{\beta\mu}n_1'''$ and $\Gamma \vdash n_1' \Rightarrow_{\beta\mu}n_1'''$ and $\Gamma \vdash n_2' \Rightarrow_{\beta\mu} n_2'''$ and $\Gamma \vdash n_2' \Rightarrow_{\beta\mu}n_2'''$ . By lemma \ref{key}, $\Gamma \vdash m([n_1'/x]n_2') \Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$, also $\Gamma \vdash (\lambda x.n_1'') n_2''\Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$.  

\

\noindent Suppose $\Gamma \vdash (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu}m([n_2''/x]n_1'') $, where $\Gamma \vdash n_1 \Rightarrow_{\beta\mu}n_1''$ and $\Gamma \vdash n_2 \Rightarrow_{\beta\mu} n_2''$. By IH, there exist $n_1''', n_2'''$ such that $\Gamma \vdash n_1'' \Rightarrow_{\beta\mu}n_1'''$ and $\Gamma \vdash n_1' \Rightarrow_{\beta\mu}n_1'''$ and $\Gamma \vdash n_2' \Rightarrow_{\beta\mu} n_2'''$ and $\Gamma \vdash n_2' \Rightarrow_{\beta\mu}n_2'''$ . By lemma \ref{key}, $\Gamma \vdash m([n_1'/x]n_2') \Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$ and $\Gamma \vdash m([n_1''/x]n_2'') \Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$.

\

\noindent The other cases are either similar to the one above or easy.

\end{proof}

\begin{lemma}
    \label{norm:sub}
$m(\vec{\mu}\vec{\mu}t) \equiv m(\vec{\mu}t)$ and $m(\vec{\mu} ([t_2/x]t_1)) \equiv m( [\vec{\mu} t_2/x]\vec{\mu} t_1)$
\end{lemma}

\begin{proof}
We can prove this using the same method as lemma \ref{norm:fun}, namely, identify $t$ and then proceed by inducton. I will not prove it here.
\end{proof}


\dbend
\begin{lemma}
\label{fp}
If $\Gamma \vdash a \to_{\beta} b$, then $\Gamma \vdash m(a)\to_{\beta\mu} m(b)$.
\end{lemma}

\begin{proof}
\noindent   We prove this by induction on the derivation(depth) of $\Gamma \vdash a \to_{\beta} b$. We list a few non-trial cases:

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash x \rightarrow_{\beta}  t}{(x \mapsto t) \in \Gamma}

\

\noindent We have $\Gamma \vdash m(x) \equiv  x \to_{\beta\mu} m(t)$. 

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash \mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto t_i) \in \mu}

\

\noindent We have $\Gamma \vdash m(\mu x_i) \equiv \mu x_i \to_{\beta\mu} m(\mu  t_i)$.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma \vdash (\lambda x.t)t' \to_{\beta} [t'/x]t}{}

\

\noindent We have $\Gamma \vdash m((\lambda x.t)t') \equiv (\lambda x.m(t))m(t') \to_{\beta\mu} m([m(t)/x]m(t')) \equiv m([t'/x]t)$(lemma \ref{norm:iden}). 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash \lambda x.t \to_{\beta} \lambda x.t'}{\Gamma \vdash t \to_{\beta}t' }

\

\noindent $\Gamma \vdash m(\lambda x.t)  \equiv  \lambda x.m(t)  \stackrel{IH}{\to_{\beta\mu}} \lambda x.m(t') \equiv m(\lambda x.t') $. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma \vdash \mu t \to_{\beta} \mu t'}{\Gamma, \tilde{\mu} \vdash t \to_{\beta}t' }

\

\noindent We want to show $\Gamma \vdash m(\mu t) \to_{\beta\mu}  m(\mu t') $. If $dom(\mu)\# FV(t)$, then $dom(\mu)\# FV(t')$. By IH, $\Gamma, \tilde{\mu} \vdash t \to_{\beta}t'$ implies $\Gamma, \tilde{\mu} \vdash m( t) \to_{\beta\mu} m(t')$. So $\Gamma \vdash m(\mu t) \equiv m(t) {\to_{\beta\mu}}  m(t') \equiv m(\mu t') $. 

\

\noindent If $dom(\mu)\cap FV(t) \not = \emptyset$, then identify $t$ as $\dot{\overrightarrow{\mu_1}}t''$, where
$t''$ does not contain any closure at head position. We do case analyze on the structure of $t''$: 

%\noindent $t \not = \m{y}{t'}{\bar{\mu}.y_i}$ since it will violate our assumption. 
\

\textbf{Case.} $t''=x_i \in dom(\dot{\overrightarrow{\mu_1}})$ or $x_i \notin dom(\dot{\overrightarrow{\mu_1}})$ or $*$, these cases will not arise.

\

\textbf{Case.} $t'' = \lambda y.t_1$, then it must be that $ t' = \dot{\overrightarrow{\mu_1}}(\lambda y.t_1')$ where $\Gamma,\tilde{\mu}, \tilde{\dot{\overrightarrow{\mu_1}}} \vdash t_1 \to_{\beta} t_1'$. So 
we get $ \Gamma \vdash \mu \dot{\overrightarrow{\mu_1}} t_1 \to_{\beta} \mu \dot{\overrightarrow{\mu_1}}t_1'$. The depth of $\Gamma \vdash \mu \dot{\overrightarrow{\mu_1}} t_1 \to_{\beta} \mu \dot{\overrightarrow{\mu_1}}t_1'$ is smaller than $\Gamma \vdash \mu \dot{\overrightarrow{\mu_1}} (\lambda y.t_1) \to_{\beta} \mu \dot{\overrightarrow{\mu_1}}(\lambda y.t_1')$. So by IH, we have $\Gamma \vdash m(\mu \dot{\overrightarrow{\mu_1}}t_1) \to_{\beta\mu} m(\mu \dot{\overrightarrow{\mu_1}}t_1')$. Thus $\Gamma \vdash m(\mu\dot{\overrightarrow{\mu_1}}(\lambda y.t_1)) \equiv \lambda y.m(\mu\dot{\overrightarrow{\mu_1}} t_1) \to_{\beta\mu} \lambda y.m(\mu\dot{\overrightarrow{\mu_1}} t_1') \equiv m(\mu\dot{\overrightarrow{\mu_1}} (\lambda y.t_1'))$. 

\

\textbf{Case.} $t'' = t_1 t_2$ and $t' = \dot{\overrightarrow{\mu_1}}(t_1' t_2)$, where $\Gamma, \tilde{\mu},\tilde{\dot{\overrightarrow{\mu_1}}} \vdash t_1 \to_{\beta} t_1'$. We have  $\Gamma \vdash \mu\dot{\overrightarrow{\mu_1}} t_1 \to_{\beta } \mu\dot{\overrightarrow{\mu_1}} t_1'$. By IH,
$\Gamma \vdash m(\mu\dot{\overrightarrow{\mu_1}} t_1) \to_{\beta \mu} m(\mu\dot{\overrightarrow{\mu_1}} t_1')$. Thus $\Gamma \vdash m(\mu\dot{\overrightarrow{\mu_1}}(t_1 t_2)) \equiv m(\mu\dot{\overrightarrow{\mu_1}} t_1) m(\mu\dot{\overrightarrow{\mu_1}} t_2) \to_{\beta \mu} m(\mu\dot{\overrightarrow{\mu_1}} t_1') m(\mu \dot{\overrightarrow{\mu_1}}t_2) \equiv m(\mu\dot{\overrightarrow{\mu_1}}(t_1' t_2))$.
For $t'' = t_1 t_2'$, where $\Gamma \vdash t_2 \to_{\beta} t_2'$, we can argue similarly. 

\

\textbf{Case.} $t'' = (\lambda y.t_1)t_2$ and $t' = \dot{\overrightarrow{\mu_1}}([t_2/y]t_1)$. $\Gamma \vdash m(\mu\dot{\overrightarrow{\mu_1}} ((\lambda y.t_1)t_2)) \equiv (\lambda y.m(\mu\dot{\overrightarrow{\mu_1}} t_1)))m(\mu \dot{\overrightarrow{\mu_1}}t_2)  \to_{\beta\mu} m( [m(\mu \dot{\overrightarrow{\mu_1}}t_2)/y] m(\mu \dot{\overrightarrow{\mu_1}} t_1)) \equiv m([\mu\dot{\overrightarrow{\mu_1}} t_2/y] \mu \dot{\overrightarrow{\mu_1}}t_1) \equiv m(\mu \dot{\overrightarrow{\mu_1}} ([t_2/y]t_1))$(lemma \ref{norm:sub}).

\textbf{Case.} $t'' = \iota x.t_1, \Pi x:t_1.t_2$. Similar as above.

 %% \textbf{Case.} $t = \mu_1 t_1$, then $t' = \mu_1 t_1'$ where $ \Gamma,\mu,\mu_1 \vdash t_1 \to_{\beta} t_1'$. We want to show $\Gamma \vdash m(\mu \mu_1 t_1) \to_{\beta\mu}^*  m(\mu \mu_1 t_1') $. Now we again do a case analysis on $t_1'$, we repeat this process, since $t$ is a finite term, we eventually will only need to show $ \Gamma \vdash m(\mu \mu_1 ....\mu_n t_n) \to_{\beta\mu}^*  m(\mu \mu_1....\mu_n t_n')$, where $t_n$ is not of the form $\mu t$. Thus we can use the argument similar to last three cases to finish our proof.  

\end{proof}

\begin{lemma}
\label{stump}
 If $\Gamma, \dot{\vec{\mu}} \vdash a \to_{\beta}b$, then $\Gamma \vdash m(\dot{\vec{\mu}}a) \to_{\beta\mu} m(\dot{\vec{\mu}}b)$. 
\end{lemma}

\begin{proof}
  By induction on derivation of $\Gamma, \dot{\vec{\mu}} \vdash a \to_{\beta}b$. 

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma, \dot{\vec{\mu}} \vdash x \rightarrow_{\beta}  t}{(x \mapsto t) \in \Gamma, \dot{\vec{\mu}}}

\

\noindent If $x \mapsto t \in \dot{\vec{\mu}}$, then $\Gamma \vdash m(\dot{\vec{\mu}}x) \equiv  \mu x \to_{\beta\mu} m(\mu t) \equiv m(\dot{\vec{\mu}} t)$. Techincally, the last equality need
to be justified, informally we can justify that by locality of $\mu$.  If $x \mapsto t \in \Gamma$, then $\Gamma \vdash m(\dot{\vec{\mu}}x) \equiv x \to_{\beta\mu} m(t) \equiv m(\dot{\vec{\mu}} t)$. 

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma,\dot{\vec{\mu}} \vdash \mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto t_i) \in \mu}

\

\noindent We have $\Gamma \vdash m(\dot{\vec{\mu}}\mu x_i) \equiv \mu x_i \to_{\beta\mu} m(\mu  t_i) \equiv m(\dot{\vec{\mu}} \mu t_i)$.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\Gamma, \dot{\vec{\mu}} \vdash (\lambda x.t)t' \to_{\beta} [t'/x]t}{}

\

\noindent We have $\Gamma \vdash m(\dot{\vec{\mu}}((\lambda x.t)t')) \equiv (\lambda x.m(\dot{\vec{\mu}}t))m(\dot{\vec{\mu}}t') \to_{\beta\mu} m([m(\dot{\vec{\mu}}t)/x]m(\dot{\vec{\mu}}t')) \equiv m([\dot{\vec{\mu}}t/x]\dot{\vec{\mu}}t') \equiv m(\dot{\vec{\mu}}([t'/x]t))$. The last two equalities are by lemma \ref{norm:iden}, lemma \ref{norm:sub}. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma, \dot{\vec{\mu}} \vdash \lambda x.t \to_{\beta} \lambda x.t'}{\Gamma, \dot{\vec{\mu}} \vdash t \to_{\beta}t' }

\

\noindent $\Gamma \vdash m(\dot{\vec{\mu}}(\lambda x.t))  \equiv  \lambda x.m(\dot{\vec{\mu}}t)  \stackrel{IH}{\to_{\beta\mu}} \lambda x.m(\dot{\vec{\mu}} t') \equiv m(\dot{\vec{\mu}}(\lambda x.t')) $. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\Gamma, \dot{\vec{\mu}} \vdash \mu t \to_{\beta} \mu t'}{\Gamma,\dot{\vec{\mu}} ,\tilde{\mu} \vdash t \to_{\beta}t' }

\

\noindent We want to show $\Gamma \vdash  m(\dot{\vec{\mu}} \mu t) \to_{\beta\mu} m(\dot{\vec{\mu}} \mu t')$. This is directly by IH. 

\

\noindent All the other cases are similar.
\end{proof}

\noindent \textbf{Note}: The lemma \ref{stump} above is suggested by Prof. Stump, a direct 
consequence is lemma \ref{fp}, which reconfirms the correctness of lemma \ref{fp}, but in 
a much simple way. 
\begin{theorem}
  $\to_{\beta} \cup \to_{\mu}$ is confluent. 
\end{theorem}
\begin{proof}
  We know by diamond property of $\Rightarrow_{\beta\mu}$, $\to_{\beta\mu}$ is confluent. Since
$\to_{\mu}$ is strongly normalizing and confluent, and by lemma \ref{fp} and Hardin's 
interpretation lemma(lemma \ref{interp}), we conclude $\to_{\beta} \cup \to_{\mu}$ is confluent. 
\end{proof}
\subsection{Soundness and Completeness of Analytic System} 
\label{red-sem}
\noindent We denote $\to_{\beta} \cup
\to_{\mu}$ by $\to$ in this section.

\begin{lemma} \label{optoan} If $\Gamma \vdash t_1 \leadsto t_2 $, then
$\Gamma \vdash  t_1 \to t_2$.  \end{lemma}

\begin{proof} \noindent By induction on derivation of $\Gamma \vdash t_1
    \leadsto t_2 $. 

\end{proof}

\begin{lemma}
\label{join} 
If $\Gamma \vdash t_1 = t_2 $, then there
exists $t_3$ such that $\Gamma \vdash t_1 \stackrel{*}{\to} t_3$ and
$\Gamma \vdash t_2 \stackrel{*}{\to} t_3 $.  
\end{lemma} 

\begin{proof}

\noindent By induction on derivation of $\Gamma \vdash t_1 = t_2$.

\

\noindent \textbf{Case:}

\

\noindent \infer{\Gamma \vdash t_1= t_2}{\Gamma \vdash t_1
\stackrel{*}{\leadsto} t_2}

\

\noindent By the lemma \ref{optoan} above, we have $\Gamma \vdash t_1
\stackrel{*}{\to} t_2$.

\

\noindent \textbf{Case:}

\

\noindent \infer{\Gamma \vdash t_1 =  t_3}{\Gamma \vdash t_2 =  t_3
&\Gamma \vdash t_1 =  t_2}

    \

\noindent By IH and confluence of $\to$.

\

\noindent The other cases are obvious.

\end{proof}

\begin{lemma} 
\label{sub} 
If $\Gamma \vdash  t_1 = t_2 $, then
$\Gamma \vdash [t/x]t_1 = [t/x]t_2$.  
\end{lemma} 
\begin{proof} 
By induction on the derivation of $\Gamma \vdash  t_1 = t_2 $.  
The only non-trivial case is the following:

\

\infer{\Gamma \vdash(\lambda y.t')v\leadsto [v/y]t'}{}

\

\noindent Since a $[t/x]v$ is still a value, we have $\Gamma \vdash (\lambda y.[t/x]t')([t/x]v) \leadsto [[t/x]v/y]([t/x]t') \equiv [t/x]([v/y]t')$.
\end{proof}

\begin{lemma} 
\label{eqsub} 
If  $\Gamma \vdash  t_1 = t_2$, then $\Gamma \vdash [t_1/x]t = [t_2/x]t $.
\end{lemma} 

\begin{proof} By induction on the structure of $t$. 

\end{proof}

\begin{lemma} 
If $\Gamma \vdash  t_1 \to t_2 $, then $\Gamma \vdash t_1 = t_2$.  

\end{lemma} 

\begin{proof} By induction on derivation of $\Gamma \vdash t_1 \to t_2 $. 
The only interesting case is:

\

\infer{\Gamma \vdash\mu t \to_{\mu} t}{dom(\mu) \#
\mathsf{FV}(t)}

\

\noindent then $\Gamma \vdash\mu t = t$. This is obvious. 
\end{proof}


\begin{lemma} If there exists $t_3$ such that $\Gamma \vdash t_1
\stackrel{*}{\to} t_3 $ and
$\Gamma \vdash  t_2 \stackrel{*}{\to} t_3 $, then $\Gamma \vdash t_1 = t_2 $.
\end{lemma}

\begin{proof} By the lemma above.


\end{proof}

\begin{theorem} 
\label{SandC} 
$\Gamma \vdash t_1 = t_2$ iff there exists
$t_3$ such that $\Gamma \vdash t_1 \stackrel{*}{\to} t_3$ and $\Gamma
\vdash t_2 \stackrel{*}{\to} t_3$. 

\end{theorem}

\begin{proof} By the lemmas above.  
\end{proof}
\begin{theorem}[Inverse Congruence on Equality] 
    \label{StrCong} 
    If $\Gamma \vdash \Pi 
x:t_1 . t_2 = \Pi x:t_1' . t_2'$, then $\Gamma \vdash  t_1 = t_1'$,  and
$\Gamma \vdash  t_2 =  t_2'$.
\end{theorem}

\begin{proof} By theorem \ref{SandC}. 

\end{proof}

\section{Confluence Analysis}
\begin{definition}
  Let $\to_1, \to_2$ be two notions of reduction. $\to_1$ (strong)commute with $\to_2$ if the following diagram holds.

\

\begin{diagram}[size=1.5em,textflow]
 & & a & & \\
 & \ldTo_1 & & \rdTo_2 &  \\
 b & &  &  & c \\
 & \rdDashto_2 & & \ldDashto_1 &  \\
 & & d & & \\
\end{diagram}


\end{definition}

\begin{proposition}[Hindley-Rosen]
  Let $\to_1, \to_2$ be two notions of reduction. Suppose both $\to_1$ and $\to_2$ are
confluent, and $\to_1^*$ commutes with $\to_2^*$. Then $\to_1 \cup \to_2$ is confluent.
\end{proposition}

\noindent See Barendregt's \cite{Barendregt:1985} Chapter 3.3, page 64. 



\begin{proposition}[Weak Commutative]
  Let $\hookrightarrow$ denote the reflexive closure of $\to$. Let $\to_1, \to_2$ be two notions of reduction. $\to_1$ weak commutes with $\to_2$ if the following diagram holds
\

\begin{diagram}[size=1.5em,textflow]
 & & a & & \\
 & \ldTo_1 & & \rdTo_2 &  \\
 b & &  &  & c \\
 & \rdDashInto_2 & & \ldDashtoo_1 &  \\
 & & d & & \\
\end{diagram}

\

If $\to_1$ weak commutes with $\to_2$, then $\to_1^*$ and $\to_2^*$ commute.
\end{proposition}

\noindent We will use this proposition heavily during this section. It is taken from Barendregt's \cite{Barendregt:1985} Chapter 3.3, page 65.
\subsection{Confluence Analysis for Self-type}
\begin{definition}[Type Reduction]
\

\noindent  $\Gamma \vdash t_1 \to_{\iota} t_2 $ if $t_1 \equiv \iota x.t' $ and $t_2 \equiv [t/x]t' $ for some fix $t \in \Lambda$. 

\end{definition}

\noindent \textbf{Note}: Type reduction is \textbf{not} defined inductively over structure of term and it does \textbf{not} build in structural congruence. %% Let $=_{\iota}$ denote the reflexive transitive symmetry closure of $\to_{\iota}$. 

\begin{lemma}[Confluence]
  $\to_{\iota}$ is confluent.
\end{lemma}
\begin{proof}
  This is obvious since $\to_{\iota}$ is deterministic. 
\end{proof}
\begin{lemma}
\label{cus}
    Let $\to$ denote $\to_{\beta}\cup \to_{\mu}$, if $\Gamma \vdash t \to t'$, then $\Gamma \vdash [t_1/x]t \to [t_1/x]t'$ for any $t_1$. 
\end{lemma}
\begin{proof}
  Obvious.
\end{proof}
\begin{lemma}
  Let $\to$ denote $\to_{\beta}\cup \to_{\mu}$, then $\to$ commutes with $\to_{\iota}$. i.e. if $\Gamma \vdash t_1 \to t_2$ and $\Gamma \vdash t_1 \to_{\iota} t_3$, then there exist $t_4$ such that $\Gamma \vdash t_2 \to_{\iota} t_4$ and $\Gamma \vdash t_3 \to t_4$. 
\end{lemma}
\begin{proof}
  Since $\Gamma \vdash t_1 \to_{\iota} t_3$, we know that $t_1 \equiv \iota x.t'$ and $t_3 \equiv [t/x]t'$. We also have $\Gamma \vdash t_1\equiv \iota x.t' \to t_2$. By inversion,
we know that $t_2 \equiv \iota x.t''$ with $\Gamma \vdash t' \to t''$. By lemma \ref{cus}, we know that 
$\Gamma \vdash [t/x]t' \to [t/x]t''$. Thus $t_4 \equiv [t/x]t''$ and $\Gamma \vdash \iota x.t'' \to_{\iota} [t/x]t''$.
\end{proof}

%% \noindent \textbf{Note}: We are lucky to get communtativity here, which I didn't realize at
%% first. But I am fine with this since luck is only for the one who prepare. 
\begin{theorem}
  $\to \cup \to_{\iota}$ is confluent. 
\end{theorem}

%% \noindent Let $=_{\beta,\mu,\iota}$ denote the reflexive transitive symmetry closure of $\to \cup \to_{\iota}$. 

%% \begin{theorem}
%%   If $\Gamma \vdash \Pi x:t_1. t_2 =_{\beta,\mu,\iota} \Pi x:t_1'.t_2'$, then
%% $\Gamma \vdash t_1 (\to \cup \to_{\iota})^* t_1'$ and $\Gamma \vdash t_2 (\to \cup \to_{\iota})^* t_2'$
%% \end{theorem}


\subsection{Confluence Analysis on Mu-Type}

\begin{definition}[Mu-type Reductions]

\

\small{
\begin{tabular}{llll}


\infer{\Gamma \vdash \mu t \to_{o} t}{\mu \in \Gamma}

&


\infer{\Gamma \vdash\lambda x.t \to_{o} \lambda x.t'}{\Gamma
\vdash t \to_{o}t' }

&
\infer{\Gamma \vdash t t' \to_{o} t'' t'}{\Gamma \vdash t
\to_{o}t''}

&

\infer{\Gamma \vdash t t' \to_{o} t t''}{\Gamma \vdash
t'\to_{o}t''}

\\

\\

\infer{\Gamma \vdash \mu t \to_{o} \mu t'}{\Gamma,\tilde{\mu}\vdash t
\to_{o}t' }

&

\infer{\Gamma \vdash \iota x.t \to_{o} \iota x.t'}{\Gamma
\vdash t \to_{o}t' }
&

\infer{\Gamma \vdash \Pi x:t_1.t_2 \to_{o} \Pi
x:t_1'.t_2'}{\Gamma \vdash t_2 \to_{o}t_2' } 

&
\infer{\Gamma \vdash \Pi x:t_1.t_2 \to_{o} \Pi
x:t_1'.t_2'}{\Gamma \vdash t_1 \to_{o}t_1' } 
\\
\end{tabular}
}
  
\end{definition}

\begin{lemma}
\label{subo}
  If $\Gamma \vdash t_1 \to_o t_2$, then $\Gamma \vdash [t/x]t_1 \to_o [t/x]t_2$.
\end{lemma}
\begin{proof}
By induction on derivaton. 
\end{proof}

\begin{lemma}
\label{subo2}
  If $\Gamma \vdash t_1 \to_o t_2$, then $\Gamma \vdash [t_1/x]t \hookrightarrow_o [t_2/x]t$.
\end{lemma}
\begin{proof}
  By induction on the structure of $t$. 
\end{proof}
\begin{lemma}
  $\to_o$ has diamond property, thus is confluent.
\end{lemma}
\begin{proof}
  Straightforward induction.
\end{proof}

\begin{lemma}
  $\to_o$ commutes with $\to_{\iota}$. 
\end{lemma}
\begin{proof}
  Suppose $\Gamma \vdash \iota x.t'\to_{\iota} [t/x]t'$ and $\Gamma \vdash \iota x.t' \to_o \iota x.t''$ with $\Gamma \vdash t' \to_o t''$. Then by lemma \ref{subo}, we have $\Gamma \vdash [t/x]t' \to_o [t/x]t''$. We also have $\Gamma \vdash \iota x.t'' \to_{\iota} [t/x]t''$. 
\end{proof}

\begin{lemma}
  $\to_o$ weak commutes with $\to_{\beta}$. 
\end{lemma}
\begin{proof}
\noindent By induction on $\to_o$.

\

\noindent \textbf{Case}: $\Gamma \vdash \mu t \to_o t$, where $\mu \in \Gamma$.

\

\noindent If $\Gamma \vdash \mu x_i \to_{\beta} \mu t_i$, where $x_i \mapsto t_i \in \mu$, then
$\Gamma \vdash \mu x_i \to_o x_i$. So we have $\Gamma \vdash \mu t_i \to_o t_i$ and $\Gamma \vdash x_i \to_{\beta} t_i$ since $\mu \in \Gamma$. 

\

\noindent If $\Gamma \vdash \mu t \to_{\beta} \mu t'$, with $\Gamma \vdash t \to_{\beta} t'$. So we have $\Gamma \vdash t \to_{\beta} t'$ and $\Gamma \vdash \mu t' \to_o t'$. 

\

\noindent \textbf{Case}: $\Gamma \vdash (\lambda x.t_1)t_2 \to_o (\lambda x.t_1')t_2$, where 
$\Gamma \vdash t_1 \to_o t_1'$. 

\

\noindent Suppose $\Gamma \vdash (\lambda x.t_1)t_2 \to_{\beta} [t_2/x]t_1$. By lemma \ref{subo}, we know that $\Gamma \vdash [t_2/x]t_1 \to_o [t_2/x]t_1'$. And we also have $\Gamma \vdash (\lambda x.t_1')t_2 \to_{\beta} [t_2/x]t_1'$. 

\

\noindent \textbf{Case}: $\Gamma \vdash (\lambda x.t_1)t_2 \to_o (\lambda x.t_1)t_2'$, where 
$\Gamma \vdash t_2 \to_o t_2'$. 

\

\noindent Suppose $\Gamma \vdash (\lambda x.t_1)t_2 \to_{\beta} [t_2/x]t_1$. By lemma \ref{subo2}, we know that $\Gamma \vdash [t_2/x]t_1 \hookrightarrow_o [t_2'/x]t_1$. And we also have $\Gamma \vdash (\lambda x.t_1)t_2' \to_{\beta} [t_2'/x]t_1$. 

\

\noindent The other cases are by induction.
\end{proof}

\begin{lemma}
$\to_o$ weak commutes with $\to_{\mu}$. i.e. if $\Gamma \vdash t \to_{o} t'$ and $\Gamma \vdash t \to_{\mu} t''$, then there exist a $t_1$ such that $\Gamma \vdash t'' \to_{o}^* t_1$ and $\Gamma \vdash t' \hookrightarrow_{\mu} t_1$.

\end{lemma}

\begin{proof}
\noindent  By induction on $\Gamma \vdash t \to_{o} t'$. 

\

\noindent \textbf{Case}: $\Gamma \vdash \mu t \to_o t$, where $\mu \in \Gamma$.

\

\noindent Suppose $\Gamma \vdash \mu t \to_{\mu} t$ with $dom(\mu) \# \mathsf{FV}(t)$. This case
is obvious. 

\

\noindent Suppose $t \equiv \lambda x.t_2$ and $\Gamma \vdash \mu (\lambda x.t_2) \to_{\mu} \lambda x.\mu t_2$. Then $\Gamma \vdash \lambda x.t_2 \hookrightarrow_{\mu} \lambda x.t_2$ and $\Gamma \vdash \lambda x.\mu t_2 \to_o \lambda x.t_2$.   

\

\noindent Suppose $t \equiv t_2 t_3$ and $\Gamma \vdash \mu (t_2 t_3) \to_{\mu} (\mu t_2)(\mu t_3)$. Then $\Gamma \vdash t_2 t_3 \hookrightarrow_{\mu} t_2 t_3$ and $\Gamma \vdash (\mu t_2)(\mu t_3) \to_o^* t_2 t_3$.

\

\noindent For $t \equiv \iota x.t_2, \Pi x:t_2.t_3$, we can argue similarly. 

\

\noindent The other cases are by induction.   
\end{proof}
\begin{theorem}
  $\to_{o} \cup \to_{\iota} \cup \to_{\beta} \cup \to_{\mu}$ is confluent.
\end{theorem}

\noindent Let $=_{\beta,\mu,\iota,o}$ denotes the reflexive transitive symmetry closure of $\to_{o} \cup \to_{\iota} \cup \to_{\beta} \cup \to_{\mu}$.

\begin{theorem}[$\iota$-elimination, or Power of Church-Rosser]
\label{invsc}
If $\Gamma \vdash \Pi x:t_1.t_2 =_{\beta,\mu,\iota,o} \Pi x:t_1'.t_2'$, then there exist $t$ such that $\Gamma \vdash \Pi x:t_1.t_2 (\to_{o} \cup \to_{\iota} \cup \to_{\beta} \cup \to_{\mu})^* t$ and $\Gamma \vdash \Pi x:t_1'.t_2' (\to_{o} \cup \to_{\iota} \cup \to_{\beta} \cup \to_{\mu})^* t$. Thus $\Gamma \vdash \Pi x:t_1.t_2 (\to_{o} \cup \to_{\beta} \cup \to_{\mu})^* t$ and $\Gamma \vdash \Pi x:t_1'.t_2' (\to_{o} \cup \to_{\beta} \cup \to_{\mu})^* t$. So $t$ must be of the form $\Pi x:t_3.t_4$ and $\Gamma \vdash t_1  (\to_{o} \cup \to_{\beta} \cup \to_{\mu})^* t_3$ and $\Gamma \vdash t_1' (\to_{o} \cup \to_{\beta} \cup \to_{\mu})^* t_3$ and $\Gamma \vdash t_2  (\to_{o} \cup \to_{\beta} \cup \to_{\mu})^* t_4$ and $\Gamma \vdash t_2' (\to_{o} \cup \to_{\beta} \cup \to_{\mu})^* t_4$. Finally, we have $\Gamma \vdash t_1 =_{\beta,\mu,o} t_1'$ and $\Gamma \vdash t_2 =_{\beta,\mu,o} t_2'$. 
\end{theorem}



\section{Applications}
\label{presv}

\noindent \textbf{Note}: In this section I use $\stackrel{t}{=}_{\beta,\mu,\iota,o}$ to mean 
the same thing as $=_{\beta,\mu,\iota,o}$, but with an emphasis on the subject $t$.

\begin{lemma}
    \label{type} If $\Gamma \vdash t_1 \stackrel{t}{=}_{\beta,\mu,\iota,o} t_2$ and $\Gamma \vdash t : t_1$ and $\Gamma \vdash t_2:*$, then $\Gamma \vdash t : t_2$.
\end{lemma}

\begin{proof} 
By induction on length of $\Gamma \vdash t_1 \stackrel{t}{=}_{\beta,\mu,\iota,o} t_2$.

\end{proof}

\begin{lemma} 
\label{conv}
 If $\Gamma \vdash t_1 \stackrel{t}{=}_{\beta,\mu,\iota,o} t_2$ and $\Gamma \vdash t = t'$, then $\Gamma \vdash t_1
\stackrel{t'}{=}_{\beta,\mu,\iota,o} t_2$.  
\end{lemma} 
\begin{proof} By induction on length of $\Gamma \vdash t_1 \stackrel{t}{=}_{\beta,\mu,\iota,o} t_2$.
\end{proof}

\begin{lemma}
    $m(\mu_1 \mu_2 t) \equiv m(\mu_2 \mu_1 t)$, thus $\Gamma \vdash \mu_1 \mu_2 t = \mu_2 \mu_1 t$.
\end{lemma}

\begin{proof}
  Identify $t$ as $\dot{\vec{\mu}} t'$, where $t'$ does not have any closure
at head position. By induction on the structure of such $t'$. Also
 $\Gamma \vdash \mu_1 \mu_2 t = m(\mu_1 \mu_2 t) = m(\mu_2 \mu_1 t) = \mu_2 \mu_1 t$. 
\end{proof}
\begin{lemma}
\label{submu}
    $\Gamma \vdash \mu ([t/x]t') = [\mu t/x] \mu t'$
\end{lemma}
\begin{proof}
$\Gamma \vdash \mu ([t/x]t') = m(\mu ([t/x]t')) = m([\mu t/x] \mu t') = [\mu t/x] \mu t'$.
\end{proof}

\begin{lemma} 
    \label{metacong} 
    If $\Gamma, \tilde{\mu} \vdash
t' \stackrel{t}{=}_{\beta,\mu,\iota,o} t''$, then $\Gamma\vdash \mu 
 t' \stackrel{\mu t }{=}_{\beta,\mu,\iota,o} \mu 
 t''$
 \end{lemma} 
 \begin{proof} By induction on length of
$\Gamma, \tilde{\mu}  \vdash t' \stackrel{t}{=}_{\beta,\mu,\iota,o} t''$. We list a few cases.

\noindent\textbf{Case}: $\Gamma, \tilde{\mu}  \vdash t' {=} t''$.

\

\noindent We have $\Gamma  \vdash \mu t'   = \mu t''$. 

\

\noindent\textbf{Case}: $\Gamma, \tilde{\mu}  \vdash \iota x.t' {\to_{\iota}} [t/x]t'$.

\

\noindent We know $\Gamma \vdash \mu \iota x.t' {=} \iota x.\mu t'  {\to_{\iota}} [\mu t/x] \mu t' {=} \mu [t/x]t'$ (the last equality is by lemma \ref{submu}). 

\end{proof}


\begin{lemma}[Inversion I] 
    If $\Gamma \vdash \lambda x.t : t'$, then $\Gamma, x: t_1 \vdash t : t_2$ 
    and $\Gamma \vdash  \Pi  x : t_1 . t_2 \stackrel{\lambda x.t}{=}_{\beta,\mu,\iota,o} t' $.

\end{lemma}

\begin{proof} By induction on the derivation of $\Gamma \vdash \lambda x.t : t'$. 

\end{proof} 

\begin{lemma}[Inversion II] 
    If $\Gamma \vdash t_1 t_2 : t'$, then
    $\Gamma \vdash t_1 : \Pi x : t_1'. t_2'$ and $\Gamma \vdash t_2 :t_1'$,  $\Gamma \vdash [t_2/x] t_2'\stackrel{ t_1
t_2} {=}_{\beta,\mu,\iota,o}  t'$.

\end{lemma}

\begin{lemma}[Inversion III] 
    If $\Gamma \vdash * : t$, then $\Gamma \vdash * \stackrel{*}{=}_{\beta,\mu,\iota,o}  t $.
\end{lemma}

\begin{lemma}[Inversion IV] 
  If $\Gamma \vdash x : t'$, then  $x:t \in \Gamma$ and $\Gamma \vdash t \stackrel{x}{=}_{\beta,\mu,\iota,o} t' $.
\end{lemma}

\begin{lemma}[Inversion V] 
 If $\Gamma, \tilde{\mu} \vdash x_j : t'$ and $x_j \in dom(\mu)$, then  $x_j:a_j \in \mu$ and $\Gamma, \tilde{\mu} \vdash a_j \stackrel{x_j}{=}_{\beta,\mu,\iota,o} t' $. 
\end{lemma}

\begin{lemma}[Inversion VI] 
    If $\Gamma  \vdash \vec{\mu}t : t'$ and $t$ does not have a closure at head position, then 
$\Gamma, \tilde{\vec{\mu}} \vdash t:t'' $ and $\Gamma  \vdash \vec{\mu}t'' \stackrel{\vec{\mu}t} {=}_{\beta,\mu,\iota,o} t' $.
\end{lemma}

\begin{lemma}[Inversion VII]
If $\Gamma \vdash \iota x.t:t'$, then $\Gamma, x:\iota x.t \vdash t:*$ and $\Gamma \vdash * \stackrel{\iota x.t}{=}_{\beta,\mu,\iota,o} t'$.
  
\end{lemma}

\begin{lemma}[Inversion VIII]
If $\Gamma \vdash \Pi x:t_1.t_2:t'$, then $\Gamma, x:t_1 \vdash t_2:*$ and $\Gamma \vdash t_1:*$ and $\Gamma \vdash * \stackrel{\Pi x:t_1.t_2}{=}_{\beta,\mu,\iota,o} t'$.
  
\end{lemma}

\subsection{Type Preservation Theorem}
%% \begin{lemma} 
%%     \label{contexteq} If $\Gamma, y:b \vdash t:a$ and $\Gamma
%% \vdash b = b'$ , then $\Gamma, y:b' \vdash t:a$.  
%% \end{lemma}
%% \begin{proof} By induction on the
%% derivation of $\Gamma,  y: b \vdash t:a$.  
%% \end{proof}


\begin{lemma} 
    \label{perm} If $\Gamma, \tilde{\mu}, y:b
\vdash t:a$ , then $\Gamma, y: \mu  b,\tilde{\mu} 
 \vdash t :a$.  
 \end{lemma}
\begin{proof} By induction on the
derivation of $\Gamma, \tilde{\mu} , y: \mu 
b \vdash t:t''$.
\end{proof}


%% \begin{lemma} 
%%     \label{dropcxt} 
%%     $\Gamma, \tilde{\mu} , y: \mu b \vdash t: t''$ iff $\Gamma, \tilde{\mu},
%% y:b \vdash t :t''$.  
%% \end{lemma} 
%% \begin{proof} 
%% By induction on the derivation. (Use the open and close rule)
%% \end{proof}

\begin{lemma}[Substitution] 
    \label{subst} If $ \Gamma_1, x:t_1, \Gamma_2\vdash  t: t_2 $
and $ \Gamma \vdash  t': t_1 $, then $  \Gamma_1, [t'/x]\Gamma_2 \vdash  [t'/x] t:[t'/x] t_2 $.
\end{lemma}

\begin{proof} By induction on the derivation of $ \Gamma_1, x:t_1, \Gamma_2\vdash  t: t_2 $
.  We will show a few nontrivial cases. 

\

\noindent \textbf{Case}: 

\

\infer{\Gamma  \vdash \iota  y. t:* }{\Gamma , y: \iota 
y .t\vdash t : *}
 
\

\noindent Let $\Gamma = \Gamma_1, x:t_1, \Gamma_2$. We want to show
$\Gamma_1,[t'/x] \Gamma_2 \vdash \iota  y. [t'/x]t : *$. By IH,
we have $\Gamma_1,[t'/x] \Gamma_2, y: \iota  y. [t'/x]t \vdash
[t'/x]t : *$. So it is the case.

\

\noindent \textbf{Case}: 

\

\infer{\Gamma  \vdash t : \iota  y. t'' }{\Gamma \vdash t :
[t/y]t'' & \Gamma  \vdash \iota  y. t'':*}

\

\noindent Let $\Gamma = \Gamma_1, x:t_1, \Gamma_2$. We want to show
$\Gamma_1,[t'/x] \Gamma_2 \vdash [t'/x]t :\iota  y. [t'/x]t'' $. By
IH, we have $\Gamma_1,[t'/x] \Gamma_2 \vdash [t'/x]t :  [
[t'/x]t/y]([t'/x]t'')$. So it is the case.

\

\noindent \textbf{Case}: 

\

\infer{\Gamma \vdash t : [t/y]t''}{\Gamma  \vdash t : \iota  y. t''
}

\

\noindent Let $\Gamma = \Gamma_1, x:t_1, \Gamma_2$. We want to show
$\Gamma_1,[t'/x] \Gamma_2 \vdash [t'/x]t :  [ [t'/x]t/y]([t'/x]t'')$. By
IH, we have $\Gamma_1,[t'/x] \Gamma_2 \vdash [t'/x]t :\iota  y.
[t'/x]t'' $. So it is the case.


%% \noindent \textbf{Case}: 

%% \

%% \infer[\textit{Open}]{\Gamma, \tilde{\mu}, \Gamma' \vdash t:  t''}{
%% \Gamma, \tilde{\mu}, \Gamma' \vdash t:\mu t'' }

%% \

%% \noindent Let $\Gamma = \Gamma_1, x:t_1, \Gamma_2$. We want to show
%% $\Gamma_1,[t'/x] \Gamma_2, [t'/x] \tilde{\mu}, [t'/x]\Gamma' \vdash [t'/x]t : [t'/x]t''$. By
%% IH, we have $\Gamma_1,[t'/x] \Gamma_2 ,[t'/x]\tilde{\mu}, [t'/x]\Gamma' \vdash [t'/x]t :\mu [t'/x]t'' $. Note we make use of the locality of $\mu$. For the case where $\Gamma' = \Gamma_1, x:t_1, \Gamma_2$, we can argue similarly.

\

\noindent \textbf{Case}: 

\

\infer[\textit{Mu}]{\Gamma \vdash \mu t: \mu t''}{\Gamma, \tilde{\mu}
\vdash t:t'' &  \{\Gamma, \tilde{\mu} \vdash t_j: a_j\}_{(t_j:a_j) \in \tilde{\mu}} }

\

\noindent Let $\Gamma = \Gamma_1, x:t_1, \Gamma_2$. We want to show
$\Gamma_1,[t'/x] \Gamma_2  \vdash \mu [t'/x]t : \mu [t'/x]t''$. By
IH, we have $\Gamma_1,[t'/x] \Gamma_2 ,[t'/x] \tilde{\mu}  \vdash [t'/x]t : [t'/x]t'' $ and
$\{\Gamma_1,[t'/x] \Gamma_2 , [t'/x]\tilde{\mu} \vdash t_j: [t'/x]a_j\}_{(t_j:[t'/x]a_j) \in [t'/x]\tilde{\mu}}$. 

\end{proof}

\begin{definition}[Well Formed Context]

\

  \begin{tabular}{lll}

\infer{\cdot \vdash \mathsf{wf}}{}
&

\infer{\Gamma, \tilde{\mu} \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf} & \{\Gamma,\tilde{\mu} \vdash t_j: a_j\}_{(t_j:a_j) \in\tilde{\mu}}  }    

&

\infer{\Gamma, x:t\vdash \mathsf{wf}}{\Gamma\vdash \mathsf{wf} & \Gamma \vdash t: * }    

  \end{tabular}


\end{definition}

\begin{theorem}[Type Preservation] If $\Gamma \vdash \mathsf{wf}$ and $ \Gamma \vdash  t \leadsto t' $ and $ \Gamma \vdash  t:
a $, then $ \Gamma \vdash  t' : a $.  
\end{theorem}

\begin{proof} \noindent By induction on the derivation of $ \Gamma \vdash  t: a $, 
We list a few nontrivial cases.

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash * : *}{}

\

\noindent This case will not arise.

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash x:a}{ x:a \in \Gamma}

\

\noindent If $\Gamma \vdash x \leadsto t'$, this means $ (x:a) \mapsto t'
\in \Gamma$ and $\Gamma \vdash t':a$ since $\Gamma \vdash \mathsf{wf}$.

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash t:t_2}{\Gamma \vdash t : t_1 & \Gamma \vdash t_1 \cong
t_2  & \Gamma \vdash t_2:*}

\

\noindent In this case  $\Gamma \vdash t \leadsto t'$. By IH, $\Gamma
\vdash t': t_1$.  Since $\Gamma \vdash t_1 \cong t_2$, we have $\Gamma \vdash
t':t_2$. 

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash t:[t/x]t''}{\Gamma \vdash t : \iota x.t'' }

\

\noindent In this case  $\Gamma \vdash t \leadsto t'$. By IH, $\Gamma
\vdash t': \iota  x.t''$. Thus we have $\Gamma \vdash t':
[t'/x]t''$. Since $\Gamma \vdash t' = t$, we have $\Gamma \vdash t':
[t/x]t''$ by Conv rule.

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash t : \iota x.t'' }{\Gamma \vdash t:[t/x]t'' & \Gamma \vdash \iota x.t'':*}

\

\noindent In this case  $\Gamma \vdash t \leadsto t'$. By IH, $\Gamma
\vdash t': [t/x]t''$. Since $\Gamma \vdash [t/x]t'' = [t'/x]t''$, we have
$\Gamma \vdash t': [t'/x]t''$.Thus we have $\Gamma \vdash t' :
\iota x.t''$. 

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash t_1' t_2' :[t_2'/x]t_2''  }{\Gamma \vdash
t_1' : \Pi x:t_1''.t_2'' & \Gamma \vdash t_2':t_1''}

\

\noindent Suppose $\Gamma \vdash (\lambda  x.t_1)v \leadsto [v/x]t_1$.
Then we know $\Gamma \vdash (\lambda  x.t_1)v : [v/x]t_2''
$ and $ \Gamma \vdash  \lambda x.t_1 : \Pi x : t_1''.t_2''$ and $ \Gamma \vdash  v :
t_1'' $. By inversion on $ \Gamma \vdash  \lambda x.t_1 : \Pi  x : t_1''. t_2'' $, we
have $ \Gamma , x:a \vdash  t_1 : b  $ and $ \Gamma \vdash  \Pi x : a.b \stackrel{\lambda  x.t_1 }{=}_{\beta,\mu,\iota,o} \Pi x: t_1''.t_2''$. By theorem \ref{invsc}, we have $\Gamma \vdash a  =_{\beta,\mu,o}  t_1'' $
and $\Gamma \vdash b =_{\beta,\mu,o} t_2''$. So we have $\Gamma, x:a \vdash t_1 :  t_2''$
and $\Gamma \vdash v :  a$. So by lemma \ref{subst}, we have $ \Gamma
\vdash  [v/x]t_1 : [v/x]t_2''$, as required. 


\

\noindent Suppose $\Gamma \vdash t_1 t_2 \leadsto t_1' t_2$, where $\Gamma
\vdash t_1 \leadsto t_1'$. We know $\Gamma \vdash t_1 t_2 : [t_2/x]t_2''$ 
and $ \Gamma \vdash  t_1 : \Pi x : t_1''.t_2''$ and $ \Gamma \vdash  t_2 :
t_1'' $. By IH, we know $ \Gamma \vdash  t_1' :  \Pi x : t_1''.t_2''$. So $\Gamma
\vdash t_1' t_2 : [t_2/x]t_2''$.

\

\noindent Suppose $\Gamma \vdash (\lambda  x.t_1) t_2 \leadsto (\lambda 
x.t_1) t_2'$, where $\Gamma \vdash t_2 \leadsto t_2'$. We know $\Gamma
\vdash (\lambda  x.t_1)t_2 : [t_2/x]t_2''$ and $ \Gamma \vdash \lambda 
x.t_1 : \Pi x : t_1''.t_2''  $ and $ \Gamma \vdash  t_2 :  t_1'' $. By IH, we know
$ \Gamma \vdash  t_2' :  t_1''  $. So $\Gamma \vdash (\lambda  x.t_1) t_2' :
[t_2'/x]t_2''$. And we know $\Gamma \vdash [t_2/x]t_2'' = [t_2'/x]t_2''$.

\

%% (\textbf{Warning}: the following cases are tedious, you could
%% potentially felt asleep if you haven't so far!)
\noindent \textbf{Case:}

\

\infer{\Gamma \vdash \mu t: \mu t'}{\Gamma, \tilde{\mu}
\vdash t:t' &  \{\Gamma, \tilde{\mu} \vdash t_j: a_j\}_{(t_j:a_j) \in \tilde{\mu} } }

\

\noindent Suppose  $\Gamma \vdash \mu x_j \leadsto \mu
t_j$, where $x_j \mapsto t_j \in \mu$. We have $\Gamma, \tilde{\mu} \vdash x_j:t'$. By
inversion, $\Gamma, \tilde{\mu} \vdash x_j:a_j$ and $\Gamma, \tilde{\mu} \vdash a_j \stackrel{x_j}{=}_{\beta,\mu,\iota,o}  t'$. 
 Since $\Gamma, \tilde{\mu} \vdash x_j = t_j$ and by lemma \ref{conv}, we   
get $\Gamma, \tilde{\mu} \vdash a_j \stackrel{t_j}{=}_{\beta,\mu,\iota,o} t'$. 
Since $\Gamma, \tilde{\mu} \vdash  t_j : a_j$, by lemma \ref{type}, $\Gamma, \tilde{\mu} \vdash t_j:t'$. Thus we have $\Gamma \vdash \mu t_j : \mu t'$.

\

\noindent Suppose  $\Gamma \vdash \mu \vec{\mu} x_j \leadsto   \mu \vec{\mu} t_j$, where $x_j \mapsto t_j  \in \mu_j$. By inversion on  $\Gamma, \tilde{\mu} \vdash \vec{\mu}x_j:t'$, we have $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash x_j:t_a$ and $\Gamma, \tilde{\mu} \vdash \vec{\mu}t_a \stackrel{\vec{\mu}x_j}{=}_{\beta,\mu,\iota,o}  t'$. By inversion on  $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash x_j:t_a$, we have $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash x_j:b$, where $(x_j:b) \in \tilde{\mu} \cup \tilde{\vec{\mu}}$ and $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash b \stackrel{x_j}{=}_{\beta,\mu,\iota,o}  t_a$. So $\Gamma \vdash \mu \vec{\mu} b \stackrel{\mu \vec{\mu} x_j}{=}_{\beta,\mu,\iota,o} \mu \vec{\mu} t_a  \stackrel{\mu \vec{\mu} x_j}{=}_{\beta,\mu,\iota,o}\mu t'$. Since $\Gamma \vdash \mu \vec{\mu} t_j:\mu \vec{\mu} b$ and $\Gamma \vdash \mu \vec{\mu} x_j = \mu \vec{\mu} t_j$, so $\Gamma \vdash \mu\vec{\mu} t_j : \mu t'$.

\

\noindent Suppose  $\Gamma\vdash \mu * \leadsto *$.
We have $\Gamma, \tilde{\mu} \vdash
* : t''$. We have $\Gamma, \tilde{\mu} \vdash * \stackrel{*}{=}_{\beta,\mu,\iota,o} t''$(by inversion). Thus we have $\Gamma \vdash  \mu *  \stackrel{\mu *}{=}_{\beta,\mu,\iota,o} \mu t''$(lemma
\ref{metacong}). We also know that $\Gamma\vdash * : *$ and
$\Gamma \vdash \mu * = *$. So we have $\Gamma
\vdash * \stackrel{\mu *}{=}_{\beta,\mu,\iota,o} \mu
 t''$. Thus $\Gamma \vdash  * \stackrel{*}{=}_{\beta,\mu,\iota,o} \mu t''$.  So $\Gamma
\vdash * : \mu t''$(lemma \ref{type}).

\

\noindent Suppose  $\Gamma\vdash \mu\vec{\mu} * \leadsto *$. We argue similarly.

\

\noindent Suppose  $\Gamma\vdash \mu x \leadsto x$, where $x \notin dom(\mu)$.
We have $\Gamma, \tilde{\mu} \vdash
x : t''$. We have $\Gamma, \tilde{\mu} \vdash a \stackrel{x}{=}_{\beta,\mu,\iota,o} t''$, where $x:a \in \Gamma$(by inversion). Thus
we have $\Gamma \vdash  \mu a  \stackrel{\mu x}{=}_{\beta,\mu,\iota,o} \mu t''$(lemma
\ref{metacong}). We also know that $\Gamma\vdash x : a$ and
$\Gamma \vdash \mu x = x$ and $\Gamma \vdash \mu a = a$. Thus $\Gamma \vdash  a
\stackrel{x}{=}_{\beta,\mu,\iota,o} \mu t''$.  So $\Gamma
\vdash x : \mu t''$(lemma \ref{type}).

\

\noindent Suppose  $\Gamma\vdash \mu \vec{\mu} x \leadsto x$, where $x \notin dom(\mu)\cup dom(\vec{\mu})$. By inversion on $\Gamma, \tilde{\mu} \vdash
\vec{\mu}x : t'$, we have $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash
x : t_a$, where $\Gamma, \tilde{\mu} \vdash \vec{\mu} t_a \stackrel{\vec{\mu} x}{=}_{\beta,\mu,\iota,o}  t'$. By inversion on $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash
x : t_a$, we have $x:b \in \Gamma$ and $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash b \stackrel{ x}{=}_{\beta,\mu,\iota,o}  t_a$. So $\Gamma,\mu \vdash  \vec{\mu} b \stackrel{  \vec{\mu} x}{=}_{\beta,\mu,\iota,o} \vec{\mu} t_a \stackrel{  \vec{\mu} x}{=}_{\beta,\mu,\iota,o} t'$. So $\Gamma \vdash  b \stackrel{  x}{=}_{\beta,\mu,\iota,o} \mu t'$. Thus $\Gamma \vdash x:\mu t'$.

\

\noindent Suppose $\Gamma\vdash \mu \lambda x.t \leadsto
\lambda  x. \mu  t$. We have $\Gamma, \tilde{\mu} \vdash \lambda  x.t : t''$ and 
$\Gamma, \tilde{\mu}, x:t_1'' \vdash t : t_2''$ and $\Gamma, \tilde{\mu} \vdash
\Pi  x:t_1''.t_2'' \stackrel{\lambda  x.t}{=}_{\beta,\mu,\iota,o}  t''$(by
inversion). Thus we have $\Gamma,x:\mu   t_1'' \vdash \mu
  t: \mu   t_2''$(lemma \ref{perm}) and
$\Gamma \vdash \mu  (\Pi  x:t_1''.t_2'') \stackrel{\mu
 \lambda  x.t}{=}_{\beta,\mu,\iota,o} \mu  t''$(lemma \ref{metacong}). By lemma \ref{conv}, $\Gamma \vdash
(\Pi  x:\mu  t_1''.\mu  t_2'')
\stackrel{\lambda  x.\mu  t}{=}_{\beta,\mu,\iota,o} \mu  t''$. Also, $\Gamma\vdash \lambda  x.\mu 
t : \Pi  x: (\mu  t_1'').(\mu 
t_2'')$.  So by lemma \ref{type}, $\Gamma\vdash \lambda 
x.\mu   t :  \mu  t''$.

\

\noindent Suppose $\Gamma\vdash \mu \vec{\mu}\lambda x.t \leadsto
\lambda  x. \mu  \vec{\mu} t$. By inversion on $\Gamma, \tilde{\mu}\vdash  \vec{\mu}(\lambda x.t): t'$, we have $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash \lambda x.t:t_a$, where $\Gamma, \tilde{\mu} \vdash \vec{\mu} t_a \stackrel{\vec{\mu} (\lambda x.t)}{=}_{\beta,\mu,\iota,o}  t'$. By inversion on $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash \lambda x.t:t_a$, then we have $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}}, x:t_1'' \vdash t : t_2''$ and $\Gamma, \tilde{\mu}, \tilde{\vec{\mu}} \vdash
\Pi  x:t_1''.t_2'' \stackrel{\lambda  x.t}{=}_{\beta,\mu,\iota,o} t_a$.
So $\Gamma, \tilde{\mu}  \vdash \Pi  x:\vec{\mu}t_1''.\vec{\mu}t_2'' \stackrel{\vec{\mu}(\lambda  x.t)}{=}_{\beta,\mu,\iota,o}\vec{\mu}t_a \stackrel{\vec{\mu}(\lambda  x.t)}{=}_{\beta,\mu,\iota,o} t' $. Thus $\Gamma  \vdash \Pi  x:\mu \vec{\mu}t_1''.\mu \vec{\mu}t_2'' \stackrel{\mu\vec{\mu}(\lambda  x.t)}{=}_{\beta,\mu,\iota,o} \mu t' $. Since $\Gamma \vdash \lambda  x.\mu\vec{\mu} t : \Pi x: \mu\vec{\mu} t_1''.\mu\vec{\mu} t_2''$, we have $\Gamma \vdash \lambda  x.\mu\vec{\mu} t : \mu t'$. 

\

\noindent Suppose $\Gamma\vdash \mu  (t_1' t_2') \leadsto (
\mu  t_1')( \mu  t_2')$. We have
$\Gamma, \tilde{\mu} \vdash t_1't_2' : t''$. We have $\Gamma,
\tilde{\mu} \vdash t_1' : \Pi  x:t_1''. t_2''$ and $\Gamma,
\tilde{\mu} \vdash t_2' : t_1''$ and $\Gamma, \tilde{\mu} \vdash  [t_2'/x]t_2''
\stackrel{t_1't_2'}{=}_{\beta,\mu,\iota,o}  t''$(by inversion). Thus we have $\Gamma
\vdash \mu   t_1':  \mu  (\Pi 
x:t_1''.t_2'')$ and $\Gamma \vdash \mu   t_2':  \mu
 t_1''$ and $\Gamma \vdash \mu 
 ([t_2'/x]t_2'') \stackrel{\mu  (t_1'
t_2')}{=}_{\beta,\mu,\iota,o}\mu  t'' $(lemma \ref{metacong}). By
lemma \ref{conv}, we have $\Gamma \vdash   
[\mu t_2'/x]\mu t_2'' \stackrel{(\mu  t_1')(\mu t_2')}{=}_{\beta,\mu,\iota,o} \mu t''$. So $\Gamma\vdash
(\mu   t_1')(\mu   t_2') :[\mu t_2'/x]\mu  t_2''$ and then $\Gamma \vdash (\mu   t_1')(\mu   t_2') : \mu t''$(lemma \ref{type}).

\

\noindent Suppose $\Gamma\vdash \mu \vec{\mu}  (t_1' t_2') \leadsto (\mu  \vec{\mu} t_1')( \mu  \vec{\mu} t_2')$, we argue similar as the case for $\Gamma\vdash \mu \vec{\mu}\lambda x.t \leadsto \lambda  x. \mu  \vec{\mu} t$. 


\



\end{proof}
\bibliographystyle{plain}
\bibliography{pts}

\appendix

\section{Well-Form Type}

\begin{lemma}
  If $\Gamma \vdash \mathsf{wf}$ and $\Gamma \vdash t:t'$, then $\Gamma \vdash t':*$.
\end{lemma}
\begin{proof}
\noindent  By induction on derivation of $\Gamma \vdash t:t'$. We list a few nontrivial cases.

\

\noindent \textbf{Case}: 

\

\infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]t'}{\Gamma
\vdash t : \iota x.t'}

\

\noindent By IH, we have $\Gamma \vdash \iota x.t':*$. So by inversion, 
we have $\Gamma , x:\iota x.t' \vdash t':*$. %% and $\Gamma \vdash * \stackrel{\iota x.t'}{=}_{\beta,\mu, \iota,o} *$. 
So by lemma \ref{subst}, we know $\Gamma \vdash [t/x]t':*$. 


\

\noindent \textbf{Case}: 

\

\infer[\textit{Lam}]{\Gamma \vdash \lambda x.t :\Pi x:t_1.
t_2}{\Gamma, x:t_1 \vdash t: t_2 & \Gamma \vdash t_1:*}

\

\noindent By IH, we know $\Gamma, x:t_1 \vdash t_2 : *$. Since $\Gamma \vdash t_1:*$, by 
\textit{Pi} rule, we have $\Gamma \vdash \Pi x:t_1.t_2:*$. 

\

\noindent \textbf{Case}: 

\

\infer[\textit{App}]{\Gamma \vdash t t':[t'/x] t_2}{\Gamma
\vdash t:\Pi x:t_1. t_2 & \Gamma \vdash t': t_1}

\

\noindent By IH, we have $\Gamma \vdash \Pi x:t_1. t_2:*$. 
By inversion on $\Gamma \vdash \Pi x:t_1. t_2:*$, we have $\Gamma, x:t_1 \vdash t_2:*$. 
So by lemma \ref{subst}, we have $\Gamma \vdash [t'/x]t_2:*$. 

\

\noindent \textbf{Case}: 

\

\infer[\textit{Mu}]{\Gamma \vdash \mu t: \mu t'}{\Gamma, \tilde{\mu}
\vdash t:t' &  \{\Gamma, \tilde{\mu} \vdash t_j: a_j\}_{(t_j:a_j) \in \tilde{\mu}} }

\

\noindent By IH, we have $\Gamma, \tilde{\mu}\vdash t':*$. So $\Gamma \vdash \mu t':\mu *$, thus
$\Gamma \vdash \mu t':*$. 

\end{proof}

\section{Progress}
\begin{lemma}
\label{val}
  If $\cdot \vdash v:\Pi x:t_1.t_2$, then $v \equiv \lambda x.t$. 
\end{lemma}

\begin{proof}
  Case analysis on $v$. Suppose $v \equiv *$. By inversion, $\cdot \vdash * : *$ 
and $\cdot \vdash * =_{\beta,\mu,\iota,o} \Pi x:t_1.t_2$, which contradicts 
Church-Rosser of $=_{\beta,\mu,\iota,o}$. Suppose $v \equiv \vec{\mu}(\Pi x:t_3.t_4)$. 
By inversion, we have $\tilde{\vec{\mu}} \vdash  \Pi x:t_3.t_4 : t_a$ and $\cdot \vdash \vec{\mu} t_a \stackrel{\vec{\mu}(\Pi x:t_3.t_4)}{=}_{\beta,\mu,\iota,o} \Pi x:t_1.t_2$. By inversion on 
$\tilde{\vec{\mu}} \vdash  \Pi x:t_3.t_4 : t_a$, we have $\tilde{\vec{\mu}} \vdash  * \stackrel{\Pi x:t_3.t_4}{=}_{\beta,\mu,\iota,o} t_a$. So we have $\cdot \vdash \vec{\mu} * \stackrel{\vec{\mu}(\Pi x:t_3.t_4)}{=}_{\beta,\mu,\iota,o} \vec{\mu} t_a \stackrel{\vec{\mu}(\Pi x:t_3.t_4)}{=}_{\beta,\mu,\iota,o} \Pi x:t_1.t_2$. Again, this contradicts Church-Rosser of $=_{\beta,\mu,\iota,o}$. For other cases like: $v \equiv \Pi x:t.t', \iota x.t, \vec{\mu}(\iota x.t)$, we argue similarly. 
\end{proof}

\begin{theorem}[Progress]
  If $\cdot \vdash t:t''$, then either $\cdot \vdash t \leadsto t'$ or $t$ is a value.
\end{theorem}

\begin{proof}
  By induction on the derivation of $\cdot \vdash t:t''$, we list a few cases.

\

%% \noindent \textbf{Case}:

%% \

%% \infer[\textit{Star}]{\cdot \vdash *:*}{}

%% \

%% \noindent Obvious.

%% \

%% \noindent \textbf{Case}:

%% \

%% \infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

%% \

%% \noindent This case will not arise.

%% \

%% \noindent \textbf{Case}:

%% \

%% \infer[\textit{Pi}]{\cdot \vdash \Pi x:t_1.t_2 : *}{x: t_1 \vdash t_2 : * & \cdot \vdash t_1 : * }

%% \

%% \noindent Obvious.

%% \

%% \noindent \textbf{Case}:

%% \

%% \infer[\textit{Self}]{\cdot \vdash \iota x.t : *}{x:\iota x.t \vdash t : * }

%% \

%% \noindent Obvious.

%% \


%% \infer[\textit{SelfInst}]{\cdot \vdash t: [t/x]t'}{\cdot \vdash t : \iota x.t'}

%% \

%% \noindent By IH. 

%% \

%% \noindent \textbf{Case}:

%% \

%% \infer[\textit{Lam}]{\cdot \vdash \lambda x.t :\Pi x:t_1.
%% t_2}{x:t_1 \vdash t: t_2 & \cdot \vdash t_1:*}

%% \

%% \noindent Obvious.

%% \

\noindent \textbf{Case}:

\

\infer[\textit{Mu}]{\cdot \vdash \mu t: \mu t'}{ \tilde{\mu}
\vdash t:t' &  \{\tilde{\mu} \vdash t_j: a_j\}_{(t_j:a_j) \in \tilde{\mu}} }

\

\noindent Identify $t$ as $\dot{\vec{\mu}} t''$, where $t''$ does not contains any closure
at head position. Case analysis on $t''$, if it is $*, x, \lambda x.t_a, t_a t_b$, then there
exist a $t'$ such that $\cdot \vdash t \leadsto t'$. If $t'' \equiv \Pi x:t_a.t_b, \iota x.t_a$,
then it is already a value. 

\

\noindent \textbf{Case}:

\

\infer[\textit{App}]{\cdot \vdash t t':[t'/x] t_2}{\cdot
\vdash t:\Pi x:t_1. t_2 & \cdot \vdash t': t_1}

\

\noindent Since $\cdot \vdash t:\Pi x:t_1. t_2 $ and $ \cdot \vdash t': t_1$, by IH, $t$ either 
steps or is a value, likewise for $t'$. If $t$ can take a step, then $t t'$ can also take a step. If $t$ is a value, by lemma \ref{val}, $t$ must be of the form $\lambda x.t_a$. So if $t'$ can
take a step, then $t t'$ can also take a step. If both $t'$ is a value, then $t t'$ can take a step.  

\end{proof}
\end{document}
